Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simpr1 1067 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → 𝑆 ∈ 𝐸) |
3 | | simpr2 1068 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → 𝑈 ∈ 𝐸) |
4 | | simpr3 1069 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → 𝑉 ∈ 𝐸) |
5 | | tendopl.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | tendopl.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
7 | | tendopl.e |
. . . . 5
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
8 | | tendopl.p |
. . . . 5
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) |
9 | 5, 6, 7, 8 | tendoplcl 36069 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) ∈ 𝐸) |
10 | 1, 3, 4, 9 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈𝑃𝑉) ∈ 𝐸) |
11 | 5, 7 | tendococl 36060 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝑈𝑃𝑉) ∈ 𝐸) → (𝑆 ∘ (𝑈𝑃𝑉)) ∈ 𝐸) |
12 | 1, 2, 10, 11 | syl3anc 1326 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ (𝑈𝑃𝑉)) ∈ 𝐸) |
13 | 5, 7 | tendococl 36060 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸) → (𝑆 ∘ 𝑈) ∈ 𝐸) |
14 | 1, 2, 3, 13 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ 𝑈) ∈ 𝐸) |
15 | 5, 7 | tendococl 36060 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑆 ∘ 𝑉) ∈ 𝐸) |
16 | 1, 2, 4, 15 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ 𝑉) ∈ 𝐸) |
17 | 5, 6, 7, 8 | tendoplcl 36069 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∘ 𝑈) ∈ 𝐸 ∧ (𝑆 ∘ 𝑉) ∈ 𝐸) → ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉)) ∈ 𝐸) |
18 | 1, 14, 16, 17 | syl3anc 1326 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉)) ∈ 𝐸) |
19 | | simplll 798 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝐾 ∈ HL) |
20 | | simpllr 799 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝑊 ∈ 𝐻) |
21 | | simplr1 1103 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝑆 ∈ 𝐸) |
22 | | simpll 790 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
23 | | simplr2 1104 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝑈 ∈ 𝐸) |
24 | | simpr 477 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ 𝑇) |
25 | 5, 6, 7 | tendocl 36055 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (𝑈‘𝑔) ∈ 𝑇) |
26 | 22, 23, 24, 25 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑈‘𝑔) ∈ 𝑇) |
27 | | simplr3 1105 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → 𝑉 ∈ 𝐸) |
28 | 5, 6, 7 | tendocl 36055 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (𝑉‘𝑔) ∈ 𝑇) |
29 | 22, 27, 24, 28 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑉‘𝑔) ∈ 𝑇) |
30 | 5, 6, 7 | tendovalco 36053 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸) ∧ ((𝑈‘𝑔) ∈ 𝑇 ∧ (𝑉‘𝑔) ∈ 𝑇)) → (𝑆‘((𝑈‘𝑔) ∘ (𝑉‘𝑔))) = ((𝑆‘(𝑈‘𝑔)) ∘ (𝑆‘(𝑉‘𝑔)))) |
31 | 19, 20, 21, 26, 29, 30 | syl32anc 1334 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑆‘((𝑈‘𝑔) ∘ (𝑉‘𝑔))) = ((𝑆‘(𝑈‘𝑔)) ∘ (𝑆‘(𝑉‘𝑔)))) |
32 | 8, 6 | tendopl2 36065 |
. . . . . . 7
⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝑔) = ((𝑈‘𝑔) ∘ (𝑉‘𝑔))) |
33 | 23, 27, 24, 32 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝑔) = ((𝑈‘𝑔) ∘ (𝑉‘𝑔))) |
34 | 33 | fveq2d 6195 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑆‘((𝑈𝑃𝑉)‘𝑔)) = (𝑆‘((𝑈‘𝑔) ∘ (𝑉‘𝑔)))) |
35 | 5, 6, 7 | tendocoval 36054 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ 𝑈)‘𝑔) = (𝑆‘(𝑈‘𝑔))) |
36 | 19, 20, 21, 23, 24, 35 | syl221anc 1337 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ 𝑈)‘𝑔) = (𝑆‘(𝑈‘𝑔))) |
37 | 5, 6, 7 | tendocoval 36054 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ 𝑉)‘𝑔) = (𝑆‘(𝑉‘𝑔))) |
38 | 19, 20, 21, 27, 24, 37 | syl221anc 1337 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ 𝑉)‘𝑔) = (𝑆‘(𝑉‘𝑔))) |
39 | 36, 38 | coeq12d 5286 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (((𝑆 ∘ 𝑈)‘𝑔) ∘ ((𝑆 ∘ 𝑉)‘𝑔)) = ((𝑆‘(𝑈‘𝑔)) ∘ (𝑆‘(𝑉‘𝑔)))) |
40 | 31, 34, 39 | 3eqtr4rd 2667 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (((𝑆 ∘ 𝑈)‘𝑔) ∘ ((𝑆 ∘ 𝑉)‘𝑔)) = (𝑆‘((𝑈𝑃𝑉)‘𝑔))) |
41 | 22, 21, 23, 13 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑆 ∘ 𝑈) ∈ 𝐸) |
42 | 22, 21, 27, 15 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑆 ∘ 𝑉) ∈ 𝐸) |
43 | 8, 6 | tendopl2 36065 |
. . . . 5
⊢ (((𝑆 ∘ 𝑈) ∈ 𝐸 ∧ (𝑆 ∘ 𝑉) ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))‘𝑔) = (((𝑆 ∘ 𝑈)‘𝑔) ∘ ((𝑆 ∘ 𝑉)‘𝑔))) |
44 | 41, 42, 24, 43 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))‘𝑔) = (((𝑆 ∘ 𝑈)‘𝑔) ∘ ((𝑆 ∘ 𝑉)‘𝑔))) |
45 | 22, 23, 27, 9 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → (𝑈𝑃𝑉) ∈ 𝐸) |
46 | 5, 6, 7 | tendocoval 36054 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ (𝑈𝑃𝑉) ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ (𝑈𝑃𝑉))‘𝑔) = (𝑆‘((𝑈𝑃𝑉)‘𝑔))) |
47 | 22, 21, 45, 24, 46 | syl121anc 1331 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ (𝑈𝑃𝑉))‘𝑔) = (𝑆‘((𝑈𝑃𝑉)‘𝑔))) |
48 | 40, 44, 47 | 3eqtr4rd 2667 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) ∧ 𝑔 ∈ 𝑇) → ((𝑆 ∘ (𝑈𝑃𝑉))‘𝑔) = (((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))‘𝑔)) |
49 | 48 | ralrimiva 2966 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ∀𝑔 ∈ 𝑇 ((𝑆 ∘ (𝑈𝑃𝑉))‘𝑔) = (((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))‘𝑔)) |
50 | 5, 6, 7 | tendoeq1 36052 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∘ (𝑈𝑃𝑉)) ∈ 𝐸 ∧ ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉)) ∈ 𝐸) ∧ ∀𝑔 ∈ 𝑇 ((𝑆 ∘ (𝑈𝑃𝑉))‘𝑔) = (((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))‘𝑔)) → (𝑆 ∘ (𝑈𝑃𝑉)) = ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))) |
51 | 1, 12, 18, 49, 50 | syl121anc 1331 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ (𝑈𝑃𝑉)) = ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))) |