Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhlveclem Structured version   Visualization version   GIF version

Theorem dvhlveclem 39979
Description: Lemma for dvhlvec 39980. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does πœ‘ β†’ method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
Hypotheses
Ref Expression
dvhgrp.b 𝐡 = (Baseβ€˜πΎ)
dvhgrp.h 𝐻 = (LHypβ€˜πΎ)
dvhgrp.t 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
dvhgrp.e 𝐸 = ((TEndoβ€˜πΎ)β€˜π‘Š)
dvhgrp.u π‘ˆ = ((DVecHβ€˜πΎ)β€˜π‘Š)
dvhgrp.d 𝐷 = (Scalarβ€˜π‘ˆ)
dvhgrp.p ⨣ = (+gβ€˜π·)
dvhgrp.a + = (+gβ€˜π‘ˆ)
dvhgrp.o 0 = (0gβ€˜π·)
dvhgrp.i 𝐼 = (invgβ€˜π·)
dvhlvec.m Γ— = (.rβ€˜π·)
dvhlvec.s Β· = ( ·𝑠 β€˜π‘ˆ)
Assertion
Ref Expression
dvhlveclem ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ π‘ˆ ∈ LVec)

Proof of Theorem dvhlveclem
Dummy variables 𝑑 𝑓 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvhgrp.h . . . . 5 𝐻 = (LHypβ€˜πΎ)
2 dvhgrp.t . . . . 5 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
3 dvhgrp.e . . . . 5 𝐸 = ((TEndoβ€˜πΎ)β€˜π‘Š)
4 dvhgrp.u . . . . 5 π‘ˆ = ((DVecHβ€˜πΎ)β€˜π‘Š)
5 eqid 2733 . . . . 5 (Baseβ€˜π‘ˆ) = (Baseβ€˜π‘ˆ)
61, 2, 3, 4, 5dvhvbase 39958 . . . 4 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (Baseβ€˜π‘ˆ) = (𝑇 Γ— 𝐸))
76eqcomd 2739 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (𝑇 Γ— 𝐸) = (Baseβ€˜π‘ˆ))
8 dvhgrp.a . . . 4 + = (+gβ€˜π‘ˆ)
98a1i 11 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ + = (+gβ€˜π‘ˆ))
10 dvhgrp.d . . . 4 𝐷 = (Scalarβ€˜π‘ˆ)
1110a1i 11 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ 𝐷 = (Scalarβ€˜π‘ˆ))
12 dvhlvec.s . . . 4 Β· = ( ·𝑠 β€˜π‘ˆ)
1312a1i 11 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ Β· = ( ·𝑠 β€˜π‘ˆ))
14 eqid 2733 . . . . 5 (Baseβ€˜π·) = (Baseβ€˜π·)
151, 3, 4, 10, 14dvhbase 39954 . . . 4 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (Baseβ€˜π·) = 𝐸)
1615eqcomd 2739 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ 𝐸 = (Baseβ€˜π·))
17 dvhgrp.p . . . 4 ⨣ = (+gβ€˜π·)
1817a1i 11 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ⨣ = (+gβ€˜π·))
19 dvhlvec.m . . . 4 Γ— = (.rβ€˜π·)
2019a1i 11 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ Γ— = (.rβ€˜π·))
21 eqid 2733 . . . . . 6 ((EDRingβ€˜πΎ)β€˜π‘Š) = ((EDRingβ€˜πΎ)β€˜π‘Š)
221, 21, 4, 10dvhsca 39953 . . . . 5 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ 𝐷 = ((EDRingβ€˜πΎ)β€˜π‘Š))
2322fveq2d 6896 . . . 4 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (1rβ€˜π·) = (1rβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)))
24 eqid 2733 . . . . 5 (1rβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)) = (1rβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))
251, 2, 21, 24erng1r 39866 . . . 4 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (1rβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)) = ( I β†Ύ 𝑇))
2623, 25eqtr2d 2774 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ( I β†Ύ 𝑇) = (1rβ€˜π·))
271, 21erngdv 39864 . . . . 5 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ((EDRingβ€˜πΎ)β€˜π‘Š) ∈ DivRing)
2822, 27eqeltrd 2834 . . . 4 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ 𝐷 ∈ DivRing)
29 drngring 20364 . . . 4 (𝐷 ∈ DivRing β†’ 𝐷 ∈ Ring)
3028, 29syl 17 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ 𝐷 ∈ Ring)
31 dvhgrp.b . . . 4 𝐡 = (Baseβ€˜πΎ)
32 dvhgrp.o . . . 4 0 = (0gβ€˜π·)
33 dvhgrp.i . . . 4 𝐼 = (invgβ€˜π·)
3431, 1, 2, 3, 4, 10, 17, 8, 32, 33dvhgrp 39978 . . 3 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ π‘ˆ ∈ Grp)
351, 2, 3, 4, 12dvhvscacl 39974 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑑) ∈ (𝑇 Γ— 𝐸))
36353impb 1116 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸)) β†’ (𝑠 Β· 𝑑) ∈ (𝑇 Γ— 𝐸))
37 simpl 484 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
38 simpr1 1195 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑠 ∈ 𝐸)
39 simpr2 1196 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑑 ∈ (𝑇 Γ— 𝐸))
40 xp1st 8007 . . . . . . . 8 (𝑑 ∈ (𝑇 Γ— 𝐸) β†’ (1st β€˜π‘‘) ∈ 𝑇)
4139, 40syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜π‘‘) ∈ 𝑇)
42 simpr3 1197 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑓 ∈ (𝑇 Γ— 𝐸))
43 xp1st 8007 . . . . . . . 8 (𝑓 ∈ (𝑇 Γ— 𝐸) β†’ (1st β€˜π‘“) ∈ 𝑇)
4442, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜π‘“) ∈ 𝑇)
451, 2, 3tendospdi1 39891 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (1st β€˜π‘‘) ∈ 𝑇 ∧ (1st β€˜π‘“) ∈ 𝑇)) β†’ (π‘ β€˜((1st β€˜π‘‘) ∘ (1st β€˜π‘“))) = ((π‘ β€˜(1st β€˜π‘‘)) ∘ (π‘ β€˜(1st β€˜π‘“))))
4637, 38, 41, 44, 45syl13anc 1373 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (π‘ β€˜((1st β€˜π‘‘) ∘ (1st β€˜π‘“))) = ((π‘ β€˜(1st β€˜π‘‘)) ∘ (π‘ β€˜(1st β€˜π‘“))))
471, 2, 3, 4, 10, 8, 17dvhvadd 39963 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 + 𝑓) = ⟨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩)
48473adantr1 1170 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 + 𝑓) = ⟨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩)
4948fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑑 + 𝑓)) = (1st β€˜βŸ¨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩))
50 fvex 6905 . . . . . . . . . 10 (1st β€˜π‘‘) ∈ V
51 fvex 6905 . . . . . . . . . 10 (1st β€˜π‘“) ∈ V
5250, 51coex 7921 . . . . . . . . 9 ((1st β€˜π‘‘) ∘ (1st β€˜π‘“)) ∈ V
53 ovex 7442 . . . . . . . . 9 ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)) ∈ V
5452, 53op1st 7983 . . . . . . . 8 (1st β€˜βŸ¨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩) = ((1st β€˜π‘‘) ∘ (1st β€˜π‘“))
5549, 54eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑑 + 𝑓)) = ((1st β€˜π‘‘) ∘ (1st β€˜π‘“)))
5655fveq2d 6896 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (π‘ β€˜(1st β€˜(𝑑 + 𝑓))) = (π‘ β€˜((1st β€˜π‘‘) ∘ (1st β€˜π‘“))))
571, 2, 3, 4, 12dvhvsca 39972 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑑) = ⟨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩)
58573adantr3 1172 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑑) = ⟨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩)
5958fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑑)) = (1st β€˜βŸ¨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩))
60 fvex 6905 . . . . . . . . 9 (π‘ β€˜(1st β€˜π‘‘)) ∈ V
61 vex 3479 . . . . . . . . . 10 𝑠 ∈ V
62 fvex 6905 . . . . . . . . . 10 (2nd β€˜π‘‘) ∈ V
6361, 62coex 7921 . . . . . . . . 9 (𝑠 ∘ (2nd β€˜π‘‘)) ∈ V
6460, 63op1st 7983 . . . . . . . 8 (1st β€˜βŸ¨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩) = (π‘ β€˜(1st β€˜π‘‘))
6559, 64eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑑)) = (π‘ β€˜(1st β€˜π‘‘)))
661, 2, 3, 4, 12dvhvsca 39972 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) = ⟨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩)
67663adantr2 1171 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) = ⟨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩)
6867fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑓)) = (1st β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩))
69 fvex 6905 . . . . . . . . 9 (π‘ β€˜(1st β€˜π‘“)) ∈ V
70 fvex 6905 . . . . . . . . . 10 (2nd β€˜π‘“) ∈ V
7161, 70coex 7921 . . . . . . . . 9 (𝑠 ∘ (2nd β€˜π‘“)) ∈ V
7269, 71op1st 7983 . . . . . . . 8 (1st β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩) = (π‘ β€˜(1st β€˜π‘“))
7368, 72eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑓)) = (π‘ β€˜(1st β€˜π‘“)))
7465, 73coeq12d 5865 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((1st β€˜(𝑠 Β· 𝑑)) ∘ (1st β€˜(𝑠 Β· 𝑓))) = ((π‘ β€˜(1st β€˜π‘‘)) ∘ (π‘ β€˜(1st β€˜π‘“))))
7546, 56, 743eqtr4d 2783 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (π‘ β€˜(1st β€˜(𝑑 + 𝑓))) = ((1st β€˜(𝑠 Β· 𝑑)) ∘ (1st β€˜(𝑠 Β· 𝑓))))
7630adantr 482 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝐷 ∈ Ring)
7716adantr 482 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝐸 = (Baseβ€˜π·))
7838, 77eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑠 ∈ (Baseβ€˜π·))
79 xp2nd 8008 . . . . . . . . . 10 (𝑑 ∈ (𝑇 Γ— 𝐸) β†’ (2nd β€˜π‘‘) ∈ 𝐸)
8039, 79syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘‘) ∈ 𝐸)
8180, 77eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘‘) ∈ (Baseβ€˜π·))
82 xp2nd 8008 . . . . . . . . . 10 (𝑓 ∈ (𝑇 Γ— 𝐸) β†’ (2nd β€˜π‘“) ∈ 𝐸)
8342, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘“) ∈ 𝐸)
8483, 77eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘“) ∈ (Baseβ€˜π·))
8514, 17, 19ringdi 20081 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Baseβ€˜π·) ∧ (2nd β€˜π‘‘) ∈ (Baseβ€˜π·) ∧ (2nd β€˜π‘“) ∈ (Baseβ€˜π·))) β†’ (𝑠 Γ— ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))) = ((𝑠 Γ— (2nd β€˜π‘‘)) ⨣ (𝑠 Γ— (2nd β€˜π‘“))))
8676, 78, 81, 84, 85syl13anc 1373 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))) = ((𝑠 Γ— (2nd β€˜π‘‘)) ⨣ (𝑠 Γ— (2nd β€˜π‘“))))
8714, 17ringacl 20095 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ (2nd β€˜π‘‘) ∈ (Baseβ€˜π·) ∧ (2nd β€˜π‘“) ∈ (Baseβ€˜π·)) β†’ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)) ∈ (Baseβ€˜π·))
8876, 81, 84, 87syl3anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)) ∈ (Baseβ€˜π·))
8988, 77eleqtrrd 2837 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)) ∈ 𝐸)
901, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)) ∈ 𝐸)) β†’ (𝑠 Γ— ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))) = (𝑠 ∘ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))))
9137, 38, 89, 90syl12anc 836 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))) = (𝑠 ∘ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))))
921, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd β€˜π‘‘) ∈ 𝐸)) β†’ (𝑠 Γ— (2nd β€˜π‘‘)) = (𝑠 ∘ (2nd β€˜π‘‘)))
9337, 38, 80, 92syl12anc 836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— (2nd β€˜π‘‘)) = (𝑠 ∘ (2nd β€˜π‘‘)))
941, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd β€˜π‘“) ∈ 𝐸)) β†’ (𝑠 Γ— (2nd β€˜π‘“)) = (𝑠 ∘ (2nd β€˜π‘“)))
9537, 38, 83, 94syl12anc 836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— (2nd β€˜π‘“)) = (𝑠 ∘ (2nd β€˜π‘“)))
9693, 95oveq12d 7427 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Γ— (2nd β€˜π‘‘)) ⨣ (𝑠 Γ— (2nd β€˜π‘“))) = ((𝑠 ∘ (2nd β€˜π‘‘)) ⨣ (𝑠 ∘ (2nd β€˜π‘“))))
9786, 91, 963eqtr3d 2781 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ∘ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))) = ((𝑠 ∘ (2nd β€˜π‘‘)) ⨣ (𝑠 ∘ (2nd β€˜π‘“))))
9848fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑑 + 𝑓)) = (2nd β€˜βŸ¨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩))
9952, 53op2nd 7984 . . . . . . . 8 (2nd β€˜βŸ¨((1st β€˜π‘‘) ∘ (1st β€˜π‘“)), ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))⟩) = ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))
10098, 99eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑑 + 𝑓)) = ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“)))
101100coeq2d 5863 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ∘ (2nd β€˜(𝑑 + 𝑓))) = (𝑠 ∘ ((2nd β€˜π‘‘) ⨣ (2nd β€˜π‘“))))
10258fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑑)) = (2nd β€˜βŸ¨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩))
10360, 63op2nd 7984 . . . . . . . 8 (2nd β€˜βŸ¨(π‘ β€˜(1st β€˜π‘‘)), (𝑠 ∘ (2nd β€˜π‘‘))⟩) = (𝑠 ∘ (2nd β€˜π‘‘))
104102, 103eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑑)) = (𝑠 ∘ (2nd β€˜π‘‘)))
10567fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑓)) = (2nd β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩))
10669, 71op2nd 7984 . . . . . . . 8 (2nd β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩) = (𝑠 ∘ (2nd β€˜π‘“))
107105, 106eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑓)) = (𝑠 ∘ (2nd β€˜π‘“)))
108104, 107oveq12d 7427 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((2nd β€˜(𝑠 Β· 𝑑)) ⨣ (2nd β€˜(𝑠 Β· 𝑓))) = ((𝑠 ∘ (2nd β€˜π‘‘)) ⨣ (𝑠 ∘ (2nd β€˜π‘“))))
10997, 101, 1083eqtr4d 2783 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ∘ (2nd β€˜(𝑑 + 𝑓))) = ((2nd β€˜(𝑠 Β· 𝑑)) ⨣ (2nd β€˜(𝑠 Β· 𝑓))))
11075, 109opeq12d 4882 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ⟨(π‘ β€˜(1st β€˜(𝑑 + 𝑓))), (𝑠 ∘ (2nd β€˜(𝑑 + 𝑓)))⟩ = ⟨((1st β€˜(𝑠 Β· 𝑑)) ∘ (1st β€˜(𝑠 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑑)) ⨣ (2nd β€˜(𝑠 Β· 𝑓)))⟩)
1111, 2, 3, 4, 10, 17, 8dvhvaddcl 39966 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 + 𝑓) ∈ (𝑇 Γ— 𝐸))
1121113adantr1 1170 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 + 𝑓) ∈ (𝑇 Γ— 𝐸))
1131, 2, 3, 4, 12dvhvsca 39972 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑑 + 𝑓) ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· (𝑑 + 𝑓)) = ⟨(π‘ β€˜(1st β€˜(𝑑 + 𝑓))), (𝑠 ∘ (2nd β€˜(𝑑 + 𝑓)))⟩)
11437, 38, 112, 113syl12anc 836 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· (𝑑 + 𝑓)) = ⟨(π‘ β€˜(1st β€˜(𝑑 + 𝑓))), (𝑠 ∘ (2nd β€˜(𝑑 + 𝑓)))⟩)
115353adantr3 1172 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑑) ∈ (𝑇 Γ— 𝐸))
1161, 2, 3, 4, 12dvhvscacl 39974 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))
1171163adantr2 1171 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))
1181, 2, 3, 4, 10, 8, 17dvhvadd 39963 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑠 Β· 𝑑) ∈ (𝑇 Γ— 𝐸) ∧ (𝑠 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Β· 𝑑) + (𝑠 Β· 𝑓)) = ⟨((1st β€˜(𝑠 Β· 𝑑)) ∘ (1st β€˜(𝑠 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑑)) ⨣ (2nd β€˜(𝑠 Β· 𝑓)))⟩)
11937, 115, 117, 118syl12anc 836 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Β· 𝑑) + (𝑠 Β· 𝑓)) = ⟨((1st β€˜(𝑠 Β· 𝑑)) ∘ (1st β€˜(𝑠 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑑)) ⨣ (2nd β€˜(𝑠 Β· 𝑓)))⟩)
120110, 114, 1193eqtr4d 2783 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ (𝑇 Γ— 𝐸) ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· (𝑑 + 𝑓)) = ((𝑠 Β· 𝑑) + (𝑠 Β· 𝑓)))
121 simpl 484 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
122 simpr1 1195 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑠 ∈ 𝐸)
123 simpr2 1196 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑑 ∈ 𝐸)
124 simpr3 1197 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑓 ∈ (𝑇 Γ— 𝐸))
125124, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜π‘“) ∈ 𝑇)
126 eqid 2733 . . . . . . . 8 (+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)) = (+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))
1271, 2, 3, 21, 126erngplus2 39675 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ (1st β€˜π‘“) ∈ 𝑇)) β†’ ((𝑠(+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))𝑑)β€˜(1st β€˜π‘“)) = ((π‘ β€˜(1st β€˜π‘“)) ∘ (π‘‘β€˜(1st β€˜π‘“))))
128121, 122, 123, 125, 127syl13anc 1373 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠(+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))𝑑)β€˜(1st β€˜π‘“)) = ((π‘ β€˜(1st β€˜π‘“)) ∘ (π‘‘β€˜(1st β€˜π‘“))))
12922fveq2d 6896 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (+gβ€˜π·) = (+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)))
13017, 129eqtrid 2785 . . . . . . . . 9 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ⨣ = (+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š)))
131130oveqd 7426 . . . . . . . 8 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (𝑠 ⨣ 𝑑) = (𝑠(+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))𝑑))
132131fveq1d 6894 . . . . . . 7 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)) = ((𝑠(+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))𝑑)β€˜(1st β€˜π‘“)))
133132adantr 482 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)) = ((𝑠(+gβ€˜((EDRingβ€˜πΎ)β€˜π‘Š))𝑑)β€˜(1st β€˜π‘“)))
134663adantr2 1171 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) = ⟨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩)
135134fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑓)) = (1st β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩))
136135, 72eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑠 Β· 𝑓)) = (π‘ β€˜(1st β€˜π‘“)))
1371, 2, 3, 4, 12dvhvsca 39972 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 Β· 𝑓) = ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩)
1381373adantr1 1170 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 Β· 𝑓) = ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩)
139138fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑑 Β· 𝑓)) = (1st β€˜βŸ¨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩))
140 fvex 6905 . . . . . . . . 9 (π‘‘β€˜(1st β€˜π‘“)) ∈ V
141 vex 3479 . . . . . . . . . 10 𝑑 ∈ V
142141, 70coex 7921 . . . . . . . . 9 (𝑑 ∘ (2nd β€˜π‘“)) ∈ V
143140, 142op1st 7983 . . . . . . . 8 (1st β€˜βŸ¨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩) = (π‘‘β€˜(1st β€˜π‘“))
144139, 143eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (1st β€˜(𝑑 Β· 𝑓)) = (π‘‘β€˜(1st β€˜π‘“)))
145136, 144coeq12d 5865 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((1st β€˜(𝑠 Β· 𝑓)) ∘ (1st β€˜(𝑑 Β· 𝑓))) = ((π‘ β€˜(1st β€˜π‘“)) ∘ (π‘‘β€˜(1st β€˜π‘“))))
146128, 133, 1453eqtr4d 2783 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)) = ((1st β€˜(𝑠 Β· 𝑓)) ∘ (1st β€˜(𝑑 Β· 𝑓))))
14730adantr 482 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝐷 ∈ Ring)
14816adantr 482 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝐸 = (Baseβ€˜π·))
149122, 148eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑠 ∈ (Baseβ€˜π·))
150123, 148eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ 𝑑 ∈ (Baseβ€˜π·))
151124, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘“) ∈ 𝐸)
152151, 148eleqtrd 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜π‘“) ∈ (Baseβ€˜π·))
15314, 17, 19ringdir 20082 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Baseβ€˜π·) ∧ 𝑑 ∈ (Baseβ€˜π·) ∧ (2nd β€˜π‘“) ∈ (Baseβ€˜π·))) β†’ ((𝑠 ⨣ 𝑑) Γ— (2nd β€˜π‘“)) = ((𝑠 Γ— (2nd β€˜π‘“)) ⨣ (𝑑 Γ— (2nd β€˜π‘“))))
154147, 149, 150, 152, 153syl13anc 1373 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) Γ— (2nd β€˜π‘“)) = ((𝑠 Γ— (2nd β€˜π‘“)) ⨣ (𝑑 Γ— (2nd β€˜π‘“))))
15514, 17ringacl 20095 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Baseβ€˜π·) ∧ 𝑑 ∈ (Baseβ€˜π·)) β†’ (𝑠 ⨣ 𝑑) ∈ (Baseβ€˜π·))
156147, 149, 150, 155syl3anc 1372 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ⨣ 𝑑) ∈ (Baseβ€˜π·))
157156, 148eleqtrrd 2837 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ⨣ 𝑑) ∈ 𝐸)
1581, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑑) ∈ 𝐸 ∧ (2nd β€˜π‘“) ∈ 𝐸)) β†’ ((𝑠 ⨣ 𝑑) Γ— (2nd β€˜π‘“)) = ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“)))
159121, 157, 151, 158syl12anc 836 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) Γ— (2nd β€˜π‘“)) = ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“)))
160121, 122, 151, 94syl12anc 836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— (2nd β€˜π‘“)) = (𝑠 ∘ (2nd β€˜π‘“)))
1611, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑑 ∈ 𝐸 ∧ (2nd β€˜π‘“) ∈ 𝐸)) β†’ (𝑑 Γ— (2nd β€˜π‘“)) = (𝑑 ∘ (2nd β€˜π‘“)))
162121, 123, 151, 161syl12anc 836 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 Γ— (2nd β€˜π‘“)) = (𝑑 ∘ (2nd β€˜π‘“)))
163160, 162oveq12d 7427 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Γ— (2nd β€˜π‘“)) ⨣ (𝑑 Γ— (2nd β€˜π‘“))) = ((𝑠 ∘ (2nd β€˜π‘“)) ⨣ (𝑑 ∘ (2nd β€˜π‘“))))
164154, 159, 1633eqtr3d 2781 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“)) = ((𝑠 ∘ (2nd β€˜π‘“)) ⨣ (𝑑 ∘ (2nd β€˜π‘“))))
165134fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑓)) = (2nd β€˜βŸ¨(π‘ β€˜(1st β€˜π‘“)), (𝑠 ∘ (2nd β€˜π‘“))⟩))
166165, 106eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑠 Β· 𝑓)) = (𝑠 ∘ (2nd β€˜π‘“)))
167138fveq2d 6896 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑑 Β· 𝑓)) = (2nd β€˜βŸ¨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩))
168140, 142op2nd 7984 . . . . . . . 8 (2nd β€˜βŸ¨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩) = (𝑑 ∘ (2nd β€˜π‘“))
169167, 168eqtrdi 2789 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (2nd β€˜(𝑑 Β· 𝑓)) = (𝑑 ∘ (2nd β€˜π‘“)))
170166, 169oveq12d 7427 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((2nd β€˜(𝑠 Β· 𝑓)) ⨣ (2nd β€˜(𝑑 Β· 𝑓))) = ((𝑠 ∘ (2nd β€˜π‘“)) ⨣ (𝑑 ∘ (2nd β€˜π‘“))))
171164, 170eqtr4d 2776 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“)) = ((2nd β€˜(𝑠 Β· 𝑓)) ⨣ (2nd β€˜(𝑑 Β· 𝑓))))
172146, 171opeq12d 4882 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ⟨((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“))⟩ = ⟨((1st β€˜(𝑠 Β· 𝑓)) ∘ (1st β€˜(𝑑 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑓)) ⨣ (2nd β€˜(𝑑 Β· 𝑓)))⟩)
1731, 2, 3, 4, 12dvhvsca 39972 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑑) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) Β· 𝑓) = ⟨((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“))⟩)
174121, 157, 124, 173syl12anc 836 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) Β· 𝑓) = ⟨((𝑠 ⨣ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ⨣ 𝑑) ∘ (2nd β€˜π‘“))⟩)
1751163adantr2 1171 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))
1761, 2, 3, 4, 12dvhvscacl 39974 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))
1771763adantr1 1170 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))
1781, 2, 3, 4, 10, 8, 17dvhvadd 39963 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑠 Β· 𝑓) ∈ (𝑇 Γ— 𝐸) ∧ (𝑑 Β· 𝑓) ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Β· 𝑓) + (𝑑 Β· 𝑓)) = ⟨((1st β€˜(𝑠 Β· 𝑓)) ∘ (1st β€˜(𝑑 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑓)) ⨣ (2nd β€˜(𝑑 Β· 𝑓)))⟩)
179121, 175, 177, 178syl12anc 836 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Β· 𝑓) + (𝑑 Β· 𝑓)) = ⟨((1st β€˜(𝑠 Β· 𝑓)) ∘ (1st β€˜(𝑑 Β· 𝑓))), ((2nd β€˜(𝑠 Β· 𝑓)) ⨣ (2nd β€˜(𝑑 Β· 𝑓)))⟩)
180172, 174, 1793eqtr4d 2783 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ⨣ 𝑑) Β· 𝑓) = ((𝑠 Β· 𝑓) + (𝑑 Β· 𝑓)))
1811, 2, 3tendocoval 39637 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸) ∧ (1st β€˜π‘“) ∈ 𝑇) β†’ ((𝑠 ∘ 𝑑)β€˜(1st β€˜π‘“)) = (π‘ β€˜(π‘‘β€˜(1st β€˜π‘“))))
182121, 122, 123, 125, 181syl121anc 1376 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ∘ 𝑑)β€˜(1st β€˜π‘“)) = (π‘ β€˜(π‘‘β€˜(1st β€˜π‘“))))
183 coass 6265 . . . . . . 7 ((𝑠 ∘ 𝑑) ∘ (2nd β€˜π‘“)) = (𝑠 ∘ (𝑑 ∘ (2nd β€˜π‘“)))
184183a1i 11 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ∘ 𝑑) ∘ (2nd β€˜π‘“)) = (𝑠 ∘ (𝑑 ∘ (2nd β€˜π‘“))))
185182, 184opeq12d 4882 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ⟨((𝑠 ∘ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ∘ 𝑑) ∘ (2nd β€˜π‘“))⟩ = ⟨(π‘ β€˜(π‘‘β€˜(1st β€˜π‘“))), (𝑠 ∘ (𝑑 ∘ (2nd β€˜π‘“)))⟩)
1861, 3tendococl 39643 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸) β†’ (𝑠 ∘ 𝑑) ∈ 𝐸)
187121, 122, 123, 186syl3anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 ∘ 𝑑) ∈ 𝐸)
1881, 2, 3, 4, 12dvhvsca 39972 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((𝑠 ∘ 𝑑) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ∘ 𝑑) Β· 𝑓) = ⟨((𝑠 ∘ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ∘ 𝑑) ∘ (2nd β€˜π‘“))⟩)
189121, 187, 124, 188syl12anc 836 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ∘ 𝑑) Β· 𝑓) = ⟨((𝑠 ∘ 𝑑)β€˜(1st β€˜π‘“)), ((𝑠 ∘ 𝑑) ∘ (2nd β€˜π‘“))⟩)
1901, 2, 3tendocl 39638 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑑 ∈ 𝐸 ∧ (1st β€˜π‘“) ∈ 𝑇) β†’ (π‘‘β€˜(1st β€˜π‘“)) ∈ 𝑇)
191121, 123, 125, 190syl3anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (π‘‘β€˜(1st β€˜π‘“)) ∈ 𝑇)
1921, 3tendococl 39643 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑑 ∈ 𝐸 ∧ (2nd β€˜π‘“) ∈ 𝐸) β†’ (𝑑 ∘ (2nd β€˜π‘“)) ∈ 𝐸)
193121, 123, 151, 192syl3anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑑 ∘ (2nd β€˜π‘“)) ∈ 𝐸)
1941, 2, 3, 4, 12dvhopvsca 39973 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (π‘‘β€˜(1st β€˜π‘“)) ∈ 𝑇 ∧ (𝑑 ∘ (2nd β€˜π‘“)) ∈ 𝐸)) β†’ (𝑠 Β· ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩) = ⟨(π‘ β€˜(π‘‘β€˜(1st β€˜π‘“))), (𝑠 ∘ (𝑑 ∘ (2nd β€˜π‘“)))⟩)
195121, 122, 191, 193, 194syl13anc 1373 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩) = ⟨(π‘ β€˜(π‘‘β€˜(1st β€˜π‘“))), (𝑠 ∘ (𝑑 ∘ (2nd β€˜π‘“)))⟩)
196185, 189, 1953eqtr4d 2783 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 ∘ 𝑑) Β· 𝑓) = (𝑠 Β· ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩))
1971, 2, 3, 4, 10, 19dvhmulr 39957 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸)) β†’ (𝑠 Γ— 𝑑) = (𝑠 ∘ 𝑑))
1981973adantr3 1172 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Γ— 𝑑) = (𝑠 ∘ 𝑑))
199198oveq1d 7424 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Γ— 𝑑) Β· 𝑓) = ((𝑠 ∘ 𝑑) Β· 𝑓))
200138oveq2d 7425 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ (𝑠 Β· (𝑑 Β· 𝑓)) = (𝑠 Β· ⟨(π‘‘β€˜(1st β€˜π‘“)), (𝑑 ∘ (2nd β€˜π‘“))⟩))
201196, 199, 2003eqtr4d 2783 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 Γ— 𝐸))) β†’ ((𝑠 Γ— 𝑑) Β· 𝑓) = (𝑠 Β· (𝑑 Β· 𝑓)))
202 xp1st 8007 . . . . . . 7 (𝑠 ∈ (𝑇 Γ— 𝐸) β†’ (1st β€˜π‘ ) ∈ 𝑇)
203202adantl 483 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (1st β€˜π‘ ) ∈ 𝑇)
204 fvresi 7171 . . . . . 6 ((1st β€˜π‘ ) ∈ 𝑇 β†’ (( I β†Ύ 𝑇)β€˜(1st β€˜π‘ )) = (1st β€˜π‘ ))
205203, 204syl 17 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (( I β†Ύ 𝑇)β€˜(1st β€˜π‘ )) = (1st β€˜π‘ ))
206 xp2nd 8008 . . . . . . 7 (𝑠 ∈ (𝑇 Γ— 𝐸) β†’ (2nd β€˜π‘ ) ∈ 𝐸)
2071, 2, 3tendof 39634 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (2nd β€˜π‘ ) ∈ 𝐸) β†’ (2nd β€˜π‘ ):π‘‡βŸΆπ‘‡)
208206, 207sylan2 594 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (2nd β€˜π‘ ):π‘‡βŸΆπ‘‡)
209 fcoi2 6767 . . . . . 6 ((2nd β€˜π‘ ):π‘‡βŸΆπ‘‡ β†’ (( I β†Ύ 𝑇) ∘ (2nd β€˜π‘ )) = (2nd β€˜π‘ ))
210208, 209syl 17 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (( I β†Ύ 𝑇) ∘ (2nd β€˜π‘ )) = (2nd β€˜π‘ ))
211205, 210opeq12d 4882 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ ⟨(( I β†Ύ 𝑇)β€˜(1st β€˜π‘ )), (( I β†Ύ 𝑇) ∘ (2nd β€˜π‘ ))⟩ = ⟨(1st β€˜π‘ ), (2nd β€˜π‘ )⟩)
2121, 2, 3tendoidcl 39640 . . . . . 6 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ ( I β†Ύ 𝑇) ∈ 𝐸)
213212anim1i 616 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (( I β†Ύ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)))
2141, 2, 3, 4, 12dvhvsca 39972 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (( I β†Ύ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 Γ— 𝐸))) β†’ (( I β†Ύ 𝑇) Β· 𝑠) = ⟨(( I β†Ύ 𝑇)β€˜(1st β€˜π‘ )), (( I β†Ύ 𝑇) ∘ (2nd β€˜π‘ ))⟩)
215213, 214syldan 592 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (( I β†Ύ 𝑇) Β· 𝑠) = ⟨(( I β†Ύ 𝑇)β€˜(1st β€˜π‘ )), (( I β†Ύ 𝑇) ∘ (2nd β€˜π‘ ))⟩)
216 1st2nd2 8014 . . . . 5 (𝑠 ∈ (𝑇 Γ— 𝐸) β†’ 𝑠 = ⟨(1st β€˜π‘ ), (2nd β€˜π‘ )⟩)
217216adantl 483 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ 𝑠 = ⟨(1st β€˜π‘ ), (2nd β€˜π‘ )⟩)
218211, 215, 2173eqtr4d 2783 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 Γ— 𝐸)) β†’ (( I β†Ύ 𝑇) Β· 𝑠) = 𝑠)
2197, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218islmodd 20477 . 2 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ π‘ˆ ∈ LMod)
22010islvec 20715 . 2 (π‘ˆ ∈ LVec ↔ (π‘ˆ ∈ LMod ∧ 𝐷 ∈ DivRing))
221219, 28, 220sylanbrc 584 1 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ π‘ˆ ∈ LVec)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βŸ¨cop 4635   I cid 5574   Γ— cxp 5675   β†Ύ cres 5679   ∘ ccom 5681  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  0gc0g 17385  invgcminusg 18820  1rcur 20004  Ringcrg 20056  DivRingcdr 20357  LModclmod 20471  LVecclvec 20713  HLchlt 38220  LHypclh 38855  LTrncltrn 38972  TEndoctendo 39623  EDRingcedring 39624  DVecHcdvh 39949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-riotaBAD 37823
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-tpos 8211  df-undef 8258  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-0g 17387  df-proset 18248  df-poset 18266  df-plt 18283  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-p0 18378  df-p1 18379  df-lat 18385  df-clat 18452  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-minusg 18823  df-mgp 19988  df-ur 20005  df-ring 20058  df-oppr 20150  df-dvdsr 20171  df-unit 20172  df-invr 20202  df-dvr 20215  df-drng 20359  df-lmod 20473  df-lvec 20714  df-oposet 38046  df-ol 38048  df-oml 38049  df-covers 38136  df-ats 38137  df-atl 38168  df-cvlat 38192  df-hlat 38221  df-llines 38369  df-lplanes 38370  df-lvols 38371  df-lines 38372  df-psubsp 38374  df-pmap 38375  df-padd 38667  df-lhyp 38859  df-laut 38860  df-ldil 38975  df-ltrn 38976  df-trl 39030  df-tendo 39626  df-edring 39628  df-dvech 39950
This theorem is referenced by:  dvhlvec  39980
  Copyright terms: Public domain W3C validator