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 38124
Description: Lemma for dvhlvec 38125. 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 2818 . . . . 5 (Base‘𝑈) = (Base‘𝑈)
61, 2, 3, 4, 5dvhvbase 38103 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝑈) = (𝑇 × 𝐸))
76eqcomd 2824 . . 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 2818 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
151, 3, 4, 10, 14dvhbase 38099 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝐷) = 𝐸)
1615eqcomd 2824 . . 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 2818 . . . . . 6 ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
221, 21, 4, 10dvhsca 38098 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊))
2322fveq2d 6667 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r𝐷) = (1r‘((EDRing‘𝐾)‘𝑊)))
24 eqid 2818 . . . . 5 (1r‘((EDRing‘𝐾)‘𝑊)) = (1r‘((EDRing‘𝐾)‘𝑊))
251, 2, 21, 24erng1r 38011 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r‘((EDRing‘𝐾)‘𝑊)) = ( I ↾ 𝑇))
2623, 25eqtr2d 2854 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) = (1r𝐷))
271, 21erngdv 38009 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing)
2822, 27eqeltrd 2910 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 ∈ DivRing)
29 drngring 19438 . . . 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 38123 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ Grp)
351, 2, 3, 4, 12dvhvscacl 38119 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
36353impb 1107 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡 ∈ (𝑇 × 𝐸)) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
37 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
38 simpr1 1186 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
39 simpr2 1187 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (𝑇 × 𝐸))
40 xp1st 7710 . . . . . . . 8 (𝑡 ∈ (𝑇 × 𝐸) → (1st𝑡) ∈ 𝑇)
4139, 40syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑡) ∈ 𝑇)
42 simpr3 1188 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
43 xp1st 7710 . . . . . . . 8 (𝑓 ∈ (𝑇 × 𝐸) → (1st𝑓) ∈ 𝑇)
4442, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
451, 2, 3tendospdi1 38036 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (1st𝑡) ∈ 𝑇 ∧ (1st𝑓) ∈ 𝑇)) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
4637, 38, 41, 44, 45syl13anc 1364 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
471, 2, 3, 4, 10, 8, 17dvhvadd 38108 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
48473adantr1 1161 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
4948fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
50 fvex 6676 . . . . . . . . . 10 (1st𝑡) ∈ V
51 fvex 6676 . . . . . . . . . 10 (1st𝑓) ∈ V
5250, 51coex 7624 . . . . . . . . 9 ((1st𝑡) ∘ (1st𝑓)) ∈ V
53 ovex 7178 . . . . . . . . 9 ((2nd𝑡) (2nd𝑓)) ∈ V
5452, 53op1st 7686 . . . . . . . 8 (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((1st𝑡) ∘ (1st𝑓))
5549, 54syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = ((1st𝑡) ∘ (1st𝑓)))
5655fveq2d 6667 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = (𝑠‘((1st𝑡) ∘ (1st𝑓))))
571, 2, 3, 4, 12dvhvsca 38117 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
58573adantr3 1163 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
5958fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
60 fvex 6676 . . . . . . . . 9 (𝑠‘(1st𝑡)) ∈ V
61 vex 3495 . . . . . . . . . 10 𝑠 ∈ V
62 fvex 6676 . . . . . . . . . 10 (2nd𝑡) ∈ V
6361, 62coex 7624 . . . . . . . . 9 (𝑠 ∘ (2nd𝑡)) ∈ V
6460, 63op1st 7686 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠‘(1st𝑡))
6559, 64syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (𝑠‘(1st𝑡)))
661, 2, 3, 4, 12dvhvsca 38117 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
67663adantr2 1162 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
6867fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
69 fvex 6676 . . . . . . . . 9 (𝑠‘(1st𝑓)) ∈ V
70 fvex 6676 . . . . . . . . . 10 (2nd𝑓) ∈ V
7161, 70coex 7624 . . . . . . . . 9 (𝑠 ∘ (2nd𝑓)) ∈ V
7269, 71op1st 7686 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠‘(1st𝑓))
7368, 72syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
7465, 73coeq12d 5728 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
7546, 56, 743eqtr4d 2863 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))))
7630adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
7716adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
7838, 77eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
79 xp2nd 7711 . . . . . . . . . 10 (𝑡 ∈ (𝑇 × 𝐸) → (2nd𝑡) ∈ 𝐸)
8039, 79syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ 𝐸)
8180, 77eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ (Base‘𝐷))
82 xp2nd 7711 . . . . . . . . . 10 (𝑓 ∈ (𝑇 × 𝐸) → (2nd𝑓) ∈ 𝐸)
8342, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
8483, 77eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
8514, 17, 19ringdi 19245 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8676, 78, 81, 84, 85syl13anc 1364 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8714, 17ringacl 19257 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷)) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8876, 81, 84, 87syl3anc 1363 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8988, 77eleqtrrd 2913 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ 𝐸)
901, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ ((2nd𝑡) (2nd𝑓)) ∈ 𝐸)) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
9137, 38, 89, 90syl12anc 832 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
921, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑡) ∈ 𝐸)) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
9337, 38, 80, 92syl12anc 832 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
941, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9537, 38, 83, 94syl12anc 832 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9693, 95oveq12d 7163 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9786, 91, 963eqtr3d 2861 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ ((2nd𝑡) (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9848fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
9952, 53op2nd 7687 . . . . . . . 8 (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((2nd𝑡) (2nd𝑓))
10098, 99syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = ((2nd𝑡) (2nd𝑓)))
101100coeq2d 5726 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
10258fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
10360, 63op2nd 7687 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠 ∘ (2nd𝑡))
104102, 103syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (𝑠 ∘ (2nd𝑡)))
10567fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
10669, 71op2nd 7687 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠 ∘ (2nd𝑓))
107105, 106syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
108104, 107oveq12d 7163 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
10997, 101, 1083eqtr4d 2863 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))))
11075, 109opeq12d 4803 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩ = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
1111, 2, 3, 4, 10, 17, 8dvhvaddcl 38111 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1121113adantr1 1161 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1131, 2, 3, 4, 12dvhvsca 38117 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
11437, 38, 112, 113syl12anc 832 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
115353adantr3 1163 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
1161, 2, 3, 4, 12dvhvscacl 38119 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1171163adantr2 1162 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1181, 2, 3, 4, 10, 8, 17dvhvadd 38108 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑡) ∈ (𝑇 × 𝐸) ∧ (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
11937, 115, 117, 118syl12anc 832 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
120110, 114, 1193eqtr4d 2863 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓)))
121 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
122 simpr1 1186 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
123 simpr2 1187 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡𝐸)
124 simpr3 1188 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
125124, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
126 eqid 2818 . . . . . . . 8 (+g‘((EDRing‘𝐾)‘𝑊)) = (+g‘((EDRing‘𝐾)‘𝑊))
1271, 2, 3, 21, 126erngplus2 37820 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇)) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
128121, 122, 123, 125, 127syl13anc 1364 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
12922fveq2d 6667 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (+g𝐷) = (+g‘((EDRing‘𝐾)‘𝑊)))
13017, 129syl5eq 2865 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → = (+g‘((EDRing‘𝐾)‘𝑊)))
131130oveqd 7162 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑠 𝑡) = (𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡))
132131fveq1d 6665 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
133132adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
134663adantr2 1162 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
135134fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
136135, 72syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
1371, 2, 3, 4, 12dvhvsca 38117 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
1381373adantr1 1161 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
139138fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
140 fvex 6676 . . . . . . . . 9 (𝑡‘(1st𝑓)) ∈ V
141 vex 3495 . . . . . . . . . 10 𝑡 ∈ V
142141, 70coex 7624 . . . . . . . . 9 (𝑡 ∘ (2nd𝑓)) ∈ V
143140, 142op1st 7686 . . . . . . . 8 (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡‘(1st𝑓))
144139, 143syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (𝑡‘(1st𝑓)))
145136, 144coeq12d 5728 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
146128, 133, 1453eqtr4d 2863 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))))
14730adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
14816adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
149122, 148eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
150123, 148eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (Base‘𝐷))
151124, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
152151, 148eleqtrd 2912 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
15314, 17, 19ringdir 19246 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
154147, 149, 150, 152, 153syl13anc 1364 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
15514, 17ringacl 19257 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷)) → (𝑠 𝑡) ∈ (Base‘𝐷))
156147, 149, 150, 155syl3anc 1363 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ (Base‘𝐷))
157156, 148eleqtrrd 2913 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ 𝐸)
1581, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 𝑡) ∈ 𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 𝑡) ∘ (2nd𝑓)))
159121, 157, 151, 158syl12anc 832 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 𝑡) ∘ (2nd𝑓)))
160121, 122, 151, 94syl12anc 832 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
1611, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
162121, 123, 151, 161syl12anc 832 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
163160, 162oveq12d 7163 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
164154, 159, 1633eqtr3d 2861 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
165134fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
166165, 106syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
167138fveq2d 6667 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
168140, 142op2nd 7687 . . . . . . . 8 (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡 ∘ (2nd𝑓))
169167, 168syl6eq 2869 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (𝑡 ∘ (2nd𝑓)))
170166, 169oveq12d 7163 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
171164, 170eqtr4d 2856 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))))
172146, 171opeq12d 4803 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩ = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
1731, 2, 3, 4, 12dvhvsca 38117 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
174121, 157, 124, 173syl12anc 832 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
1751163adantr2 1162 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1761, 2, 3, 4, 12dvhvscacl 38119 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1771763adantr1 1161 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1781, 2, 3, 4, 10, 8, 17dvhvadd 38108 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑓) ∈ (𝑇 × 𝐸) ∧ (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
179121, 175, 177, 178syl12anc 832 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
180172, 174, 1793eqtr4d 2863 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓)))
1811, 2, 3tendocoval 37782 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸) ∧ (1st𝑓) ∈ 𝑇) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
182121, 122, 123, 125, 181syl121anc 1367 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
183 coass 6111 . . . . . . 7 ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))
184183a1i 11 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓))))
185182, 184opeq12d 4803 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩ = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
1861, 3tendococl 37788 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡𝐸) → (𝑠𝑡) ∈ 𝐸)
187121, 122, 123, 186syl3anc 1363 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠𝑡) ∈ 𝐸)
1881, 2, 3, 4, 12dvhvsca 38117 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
189121, 187, 124, 188syl12anc 832 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
1901, 2, 3tendocl 37783 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇) → (𝑡‘(1st𝑓)) ∈ 𝑇)
191121, 123, 125, 190syl3anc 1363 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡‘(1st𝑓)) ∈ 𝑇)
1921, 3tendococl 37788 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
193121, 123, 151, 192syl3anc 1363 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
1941, 2, 3, 4, 12dvhopvsca 38118 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡‘(1st𝑓)) ∈ 𝑇 ∧ (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
195121, 122, 191, 193, 194syl13anc 1364 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
196185, 189, 1953eqtr4d 2863 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
1971, 2, 3, 4, 10, 19dvhmulr 38102 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸)) → (𝑠 × 𝑡) = (𝑠𝑡))
1981973adantr3 1163 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × 𝑡) = (𝑠𝑡))
199198oveq1d 7160 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠𝑡) · 𝑓))
200138oveq2d 7161 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
201196, 199, 2003eqtr4d 2863 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓)))
202 xp1st 7710 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (1st𝑠) ∈ 𝑇)
203202adantl 482 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (1st𝑠) ∈ 𝑇)
204 fvresi 6927 . . . . . 6 ((1st𝑠) ∈ 𝑇 → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
205203, 204syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
206 xp2nd 7711 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (2nd𝑠) ∈ 𝐸)
2071, 2, 3tendof 37779 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (2nd𝑠) ∈ 𝐸) → (2nd𝑠):𝑇𝑇)
208206, 207sylan2 592 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (2nd𝑠):𝑇𝑇)
209 fcoi2 6546 . . . . . 6 ((2nd𝑠):𝑇𝑇 → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
210208, 209syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
211205, 210opeq12d 4803 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩ = ⟨(1st𝑠), (2nd𝑠)⟩)
2121, 2, 3tendoidcl 37785 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
213212anim1i 614 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸)))
2141, 2, 3, 4, 12dvhvsca 38117 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸))) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
215213, 214syldan 591 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
216 1st2nd2 7717 . . . . 5 (𝑠 ∈ (𝑇 × 𝐸) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
217216adantl 482 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
218211, 215, 2173eqtr4d 2863 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 𝑠)
2197, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218islmodd 19569 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LMod)
22010islvec 19805 . 2 (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing))
221219, 28, 220sylanbrc 583 1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  cop 4563   I cid 5452   × cxp 5546  cres 5550  ccom 5552  wf 6344  cfv 6348  (class class class)co 7145  1st c1st 7676  2nd c2nd 7677  Basecbs 16471  +gcplusg 16553  .rcmulr 16554  Scalarcsca 16556   ·𝑠 cvsca 16557  0gc0g 16701  invgcminusg 18042  1rcur 19180  Ringcrg 19226  DivRingcdr 19431  LModclmod 19563  LVecclvec 19803  HLchlt 36366  LHypclh 37000  LTrncltrn 37117  TEndoctendo 37768  EDRingcedring 37769  DVecHcdvh 38094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-riotaBAD 35969
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-tpos 7881  df-undef 7928  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12881  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-sca 16569  df-vsca 16570  df-0g 16703  df-proset 17526  df-poset 17544  df-plt 17556  df-lub 17572  df-glb 17573  df-join 17574  df-meet 17575  df-p0 17637  df-p1 17638  df-lat 17644  df-clat 17706  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044  df-minusg 18045  df-mgp 19169  df-ur 19181  df-ring 19228  df-oppr 19302  df-dvdsr 19320  df-unit 19321  df-invr 19351  df-dvr 19362  df-drng 19433  df-lmod 19565  df-lvec 19804  df-oposet 36192  df-ol 36194  df-oml 36195  df-covers 36282  df-ats 36283  df-atl 36314  df-cvlat 36338  df-hlat 36367  df-llines 36514  df-lplanes 36515  df-lvols 36516  df-lines 36517  df-psubsp 36519  df-pmap 36520  df-padd 36812  df-lhyp 37004  df-laut 37005  df-ldil 37120  df-ltrn 37121  df-trl 37175  df-tendo 37771  df-edring 37773  df-dvech 38095
This theorem is referenced by:  dvhlvec  38125
  Copyright terms: Public domain W3C validator