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 39122
Description: Lemma for dvhlvec 39123. 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 2738 . . . . 5 (Base‘𝑈) = (Base‘𝑈)
61, 2, 3, 4, 5dvhvbase 39101 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝑈) = (𝑇 × 𝐸))
76eqcomd 2744 . . 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 2738 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
151, 3, 4, 10, 14dvhbase 39097 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝐷) = 𝐸)
1615eqcomd 2744 . . 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 2738 . . . . . 6 ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
221, 21, 4, 10dvhsca 39096 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊))
2322fveq2d 6778 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r𝐷) = (1r‘((EDRing‘𝐾)‘𝑊)))
24 eqid 2738 . . . . 5 (1r‘((EDRing‘𝐾)‘𝑊)) = (1r‘((EDRing‘𝐾)‘𝑊))
251, 2, 21, 24erng1r 39009 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r‘((EDRing‘𝐾)‘𝑊)) = ( I ↾ 𝑇))
2623, 25eqtr2d 2779 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) = (1r𝐷))
271, 21erngdv 39007 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing)
2822, 27eqeltrd 2839 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 ∈ DivRing)
29 drngring 19998 . . . 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 39121 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ Grp)
351, 2, 3, 4, 12dvhvscacl 39117 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
36353impb 1114 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡 ∈ (𝑇 × 𝐸)) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
37 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
38 simpr1 1193 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
39 simpr2 1194 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (𝑇 × 𝐸))
40 xp1st 7863 . . . . . . . 8 (𝑡 ∈ (𝑇 × 𝐸) → (1st𝑡) ∈ 𝑇)
4139, 40syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑡) ∈ 𝑇)
42 simpr3 1195 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
43 xp1st 7863 . . . . . . . 8 (𝑓 ∈ (𝑇 × 𝐸) → (1st𝑓) ∈ 𝑇)
4442, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
451, 2, 3tendospdi1 39034 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (1st𝑡) ∈ 𝑇 ∧ (1st𝑓) ∈ 𝑇)) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
4637, 38, 41, 44, 45syl13anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
471, 2, 3, 4, 10, 8, 17dvhvadd 39106 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
48473adantr1 1168 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
4948fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
50 fvex 6787 . . . . . . . . . 10 (1st𝑡) ∈ V
51 fvex 6787 . . . . . . . . . 10 (1st𝑓) ∈ V
5250, 51coex 7777 . . . . . . . . 9 ((1st𝑡) ∘ (1st𝑓)) ∈ V
53 ovex 7308 . . . . . . . . 9 ((2nd𝑡) (2nd𝑓)) ∈ V
5452, 53op1st 7839 . . . . . . . 8 (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((1st𝑡) ∘ (1st𝑓))
5549, 54eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = ((1st𝑡) ∘ (1st𝑓)))
5655fveq2d 6778 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = (𝑠‘((1st𝑡) ∘ (1st𝑓))))
571, 2, 3, 4, 12dvhvsca 39115 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
58573adantr3 1170 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
5958fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
60 fvex 6787 . . . . . . . . 9 (𝑠‘(1st𝑡)) ∈ V
61 vex 3436 . . . . . . . . . 10 𝑠 ∈ V
62 fvex 6787 . . . . . . . . . 10 (2nd𝑡) ∈ V
6361, 62coex 7777 . . . . . . . . 9 (𝑠 ∘ (2nd𝑡)) ∈ V
6460, 63op1st 7839 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠‘(1st𝑡))
6559, 64eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (𝑠‘(1st𝑡)))
661, 2, 3, 4, 12dvhvsca 39115 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
67663adantr2 1169 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
6867fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
69 fvex 6787 . . . . . . . . 9 (𝑠‘(1st𝑓)) ∈ V
70 fvex 6787 . . . . . . . . . 10 (2nd𝑓) ∈ V
7161, 70coex 7777 . . . . . . . . 9 (𝑠 ∘ (2nd𝑓)) ∈ V
7269, 71op1st 7839 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠‘(1st𝑓))
7368, 72eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
7465, 73coeq12d 5773 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
7546, 56, 743eqtr4d 2788 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))))
7630adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
7716adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
7838, 77eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
79 xp2nd 7864 . . . . . . . . . 10 (𝑡 ∈ (𝑇 × 𝐸) → (2nd𝑡) ∈ 𝐸)
8039, 79syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ 𝐸)
8180, 77eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ (Base‘𝐷))
82 xp2nd 7864 . . . . . . . . . 10 (𝑓 ∈ (𝑇 × 𝐸) → (2nd𝑓) ∈ 𝐸)
8342, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
8483, 77eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
8514, 17, 19ringdi 19805 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8676, 78, 81, 84, 85syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8714, 17ringacl 19817 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷)) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8876, 81, 84, 87syl3anc 1370 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8988, 77eleqtrrd 2842 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ 𝐸)
901, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ ((2nd𝑡) (2nd𝑓)) ∈ 𝐸)) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
9137, 38, 89, 90syl12anc 834 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
921, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑡) ∈ 𝐸)) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
9337, 38, 80, 92syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
941, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9537, 38, 83, 94syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9693, 95oveq12d 7293 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9786, 91, 963eqtr3d 2786 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ ((2nd𝑡) (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9848fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
9952, 53op2nd 7840 . . . . . . . 8 (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((2nd𝑡) (2nd𝑓))
10098, 99eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = ((2nd𝑡) (2nd𝑓)))
101100coeq2d 5771 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
10258fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
10360, 63op2nd 7840 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠 ∘ (2nd𝑡))
104102, 103eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (𝑠 ∘ (2nd𝑡)))
10567fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
10669, 71op2nd 7840 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠 ∘ (2nd𝑓))
107105, 106eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
108104, 107oveq12d 7293 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
10997, 101, 1083eqtr4d 2788 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))))
11075, 109opeq12d 4812 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩ = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
1111, 2, 3, 4, 10, 17, 8dvhvaddcl 39109 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1121113adantr1 1168 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1131, 2, 3, 4, 12dvhvsca 39115 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
11437, 38, 112, 113syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
115353adantr3 1170 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
1161, 2, 3, 4, 12dvhvscacl 39117 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1171163adantr2 1169 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1181, 2, 3, 4, 10, 8, 17dvhvadd 39106 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑡) ∈ (𝑇 × 𝐸) ∧ (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
11937, 115, 117, 118syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
120110, 114, 1193eqtr4d 2788 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓)))
121 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
122 simpr1 1193 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
123 simpr2 1194 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡𝐸)
124 simpr3 1195 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
125124, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
126 eqid 2738 . . . . . . . 8 (+g‘((EDRing‘𝐾)‘𝑊)) = (+g‘((EDRing‘𝐾)‘𝑊))
1271, 2, 3, 21, 126erngplus2 38818 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇)) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
128121, 122, 123, 125, 127syl13anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
12922fveq2d 6778 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (+g𝐷) = (+g‘((EDRing‘𝐾)‘𝑊)))
13017, 129eqtrid 2790 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → = (+g‘((EDRing‘𝐾)‘𝑊)))
131130oveqd 7292 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑠 𝑡) = (𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡))
132131fveq1d 6776 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
133132adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
134663adantr2 1169 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
135134fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
136135, 72eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
1371, 2, 3, 4, 12dvhvsca 39115 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
1381373adantr1 1168 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
139138fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
140 fvex 6787 . . . . . . . . 9 (𝑡‘(1st𝑓)) ∈ V
141 vex 3436 . . . . . . . . . 10 𝑡 ∈ V
142141, 70coex 7777 . . . . . . . . 9 (𝑡 ∘ (2nd𝑓)) ∈ V
143140, 142op1st 7839 . . . . . . . 8 (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡‘(1st𝑓))
144139, 143eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (𝑡‘(1st𝑓)))
145136, 144coeq12d 5773 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
146128, 133, 1453eqtr4d 2788 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))))
14730adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
14816adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
149122, 148eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
150123, 148eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (Base‘𝐷))
151124, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
152151, 148eleqtrd 2841 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
15314, 17, 19ringdir 19806 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
154147, 149, 150, 152, 153syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
15514, 17ringacl 19817 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷)) → (𝑠 𝑡) ∈ (Base‘𝐷))
156147, 149, 150, 155syl3anc 1370 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ (Base‘𝐷))
157156, 148eleqtrrd 2842 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ 𝐸)
1581, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 𝑡) ∈ 𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 𝑡) ∘ (2nd𝑓)))
159121, 157, 151, 158syl12anc 834 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 𝑡) ∘ (2nd𝑓)))
160121, 122, 151, 94syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
1611, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
162121, 123, 151, 161syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
163160, 162oveq12d 7293 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
164154, 159, 1633eqtr3d 2786 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
165134fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
166165, 106eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
167138fveq2d 6778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
168140, 142op2nd 7840 . . . . . . . 8 (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡 ∘ (2nd𝑓))
169167, 168eqtrdi 2794 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (𝑡 ∘ (2nd𝑓)))
170166, 169oveq12d 7293 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
171164, 170eqtr4d 2781 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))))
172146, 171opeq12d 4812 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩ = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
1731, 2, 3, 4, 12dvhvsca 39115 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
174121, 157, 124, 173syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
1751163adantr2 1169 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1761, 2, 3, 4, 12dvhvscacl 39117 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1771763adantr1 1168 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1781, 2, 3, 4, 10, 8, 17dvhvadd 39106 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑓) ∈ (𝑇 × 𝐸) ∧ (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
179121, 175, 177, 178syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
180172, 174, 1793eqtr4d 2788 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓)))
1811, 2, 3tendocoval 38780 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸) ∧ (1st𝑓) ∈ 𝑇) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
182121, 122, 123, 125, 181syl121anc 1374 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
183 coass 6169 . . . . . . 7 ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))
184183a1i 11 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓))))
185182, 184opeq12d 4812 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩ = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
1861, 3tendococl 38786 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡𝐸) → (𝑠𝑡) ∈ 𝐸)
187121, 122, 123, 186syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠𝑡) ∈ 𝐸)
1881, 2, 3, 4, 12dvhvsca 39115 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
189121, 187, 124, 188syl12anc 834 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
1901, 2, 3tendocl 38781 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇) → (𝑡‘(1st𝑓)) ∈ 𝑇)
191121, 123, 125, 190syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡‘(1st𝑓)) ∈ 𝑇)
1921, 3tendococl 38786 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
193121, 123, 151, 192syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
1941, 2, 3, 4, 12dvhopvsca 39116 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡‘(1st𝑓)) ∈ 𝑇 ∧ (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
195121, 122, 191, 193, 194syl13anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
196185, 189, 1953eqtr4d 2788 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
1971, 2, 3, 4, 10, 19dvhmulr 39100 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸)) → (𝑠 × 𝑡) = (𝑠𝑡))
1981973adantr3 1170 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × 𝑡) = (𝑠𝑡))
199198oveq1d 7290 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠𝑡) · 𝑓))
200138oveq2d 7291 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
201196, 199, 2003eqtr4d 2788 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓)))
202 xp1st 7863 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (1st𝑠) ∈ 𝑇)
203202adantl 482 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (1st𝑠) ∈ 𝑇)
204 fvresi 7045 . . . . . 6 ((1st𝑠) ∈ 𝑇 → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
205203, 204syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
206 xp2nd 7864 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (2nd𝑠) ∈ 𝐸)
2071, 2, 3tendof 38777 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (2nd𝑠) ∈ 𝐸) → (2nd𝑠):𝑇𝑇)
208206, 207sylan2 593 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (2nd𝑠):𝑇𝑇)
209 fcoi2 6649 . . . . . 6 ((2nd𝑠):𝑇𝑇 → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
210208, 209syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
211205, 210opeq12d 4812 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩ = ⟨(1st𝑠), (2nd𝑠)⟩)
2121, 2, 3tendoidcl 38783 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
213212anim1i 615 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸)))
2141, 2, 3, 4, 12dvhvsca 39115 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸))) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
215213, 214syldan 591 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
216 1st2nd2 7870 . . . . 5 (𝑠 ∈ (𝑇 × 𝐸) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
217216adantl 482 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
218211, 215, 2173eqtr4d 2788 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 𝑠)
2197, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218islmodd 20129 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LMod)
22010islvec 20366 . 2 (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing))
221219, 28, 220sylanbrc 583 1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1539  wcel 2106  cop 4567   I cid 5488   × cxp 5587  cres 5591  ccom 5593  wf 6429  cfv 6433  (class class class)co 7275  1st c1st 7829  2nd c2nd 7830  Basecbs 16912  +gcplusg 16962  .rcmulr 16963  Scalarcsca 16965   ·𝑠 cvsca 16966  0gc0g 17150  invgcminusg 18578  1rcur 19737  Ringcrg 19783  DivRingcdr 19991  LModclmod 20123  LVecclvec 20364  HLchlt 37364  LHypclh 37998  LTrncltrn 38115  TEndoctendo 38766  EDRingcedring 38767  DVecHcdvh 39092
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-riotaBAD 36967
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-tpos 8042  df-undef 8089  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-sca 16978  df-vsca 16979  df-0g 17152  df-proset 18013  df-poset 18031  df-plt 18048  df-lub 18064  df-glb 18065  df-join 18066  df-meet 18067  df-p0 18143  df-p1 18144  df-lat 18150  df-clat 18217  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-minusg 18581  df-mgp 19721  df-ur 19738  df-ring 19785  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-invr 19914  df-dvr 19925  df-drng 19993  df-lmod 20125  df-lvec 20365  df-oposet 37190  df-ol 37192  df-oml 37193  df-covers 37280  df-ats 37281  df-atl 37312  df-cvlat 37336  df-hlat 37365  df-llines 37512  df-lplanes 37513  df-lvols 37514  df-lines 37515  df-psubsp 37517  df-pmap 37518  df-padd 37810  df-lhyp 38002  df-laut 38003  df-ldil 38118  df-ltrn 38119  df-trl 38173  df-tendo 38769  df-edring 38771  df-dvech 39093
This theorem is referenced by:  dvhlvec  39123
  Copyright terms: Public domain W3C validator