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 38111
Description: Lemma for dvhlvec 38112. 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 2826 . . . . 5 (Base‘𝑈) = (Base‘𝑈)
61, 2, 3, 4, 5dvhvbase 38090 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝑈) = (𝑇 × 𝐸))
76eqcomd 2832 . . 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 2826 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
151, 3, 4, 10, 14dvhbase 38086 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝐷) = 𝐸)
1615eqcomd 2832 . . 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 2826 . . . . . 6 ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
221, 21, 4, 10dvhsca 38085 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊))
2322fveq2d 6671 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r𝐷) = (1r‘((EDRing‘𝐾)‘𝑊)))
24 eqid 2826 . . . . 5 (1r‘((EDRing‘𝐾)‘𝑊)) = (1r‘((EDRing‘𝐾)‘𝑊))
251, 2, 21, 24erng1r 37998 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (1r‘((EDRing‘𝐾)‘𝑊)) = ( I ↾ 𝑇))
2623, 25eqtr2d 2862 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) = (1r𝐷))
271, 21erngdv 37996 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing)
2822, 27eqeltrd 2918 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 ∈ DivRing)
29 drngring 19429 . . . 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 38110 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ Grp)
351, 2, 3, 4, 12dvhvscacl 38106 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
36353impb 1109 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡 ∈ (𝑇 × 𝐸)) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
37 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
38 simpr1 1188 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
39 simpr2 1189 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (𝑇 × 𝐸))
40 xp1st 7712 . . . . . . . 8 (𝑡 ∈ (𝑇 × 𝐸) → (1st𝑡) ∈ 𝑇)
4139, 40syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑡) ∈ 𝑇)
42 simpr3 1190 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
43 xp1st 7712 . . . . . . . 8 (𝑓 ∈ (𝑇 × 𝐸) → (1st𝑓) ∈ 𝑇)
4442, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
451, 2, 3tendospdi1 38023 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (1st𝑡) ∈ 𝑇 ∧ (1st𝑓) ∈ 𝑇)) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
4637, 38, 41, 44, 45syl13anc 1366 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘((1st𝑡) ∘ (1st𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
471, 2, 3, 4, 10, 8, 17dvhvadd 38095 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
48473adantr1 1163 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = ⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩)
4948fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
50 fvex 6680 . . . . . . . . . 10 (1st𝑡) ∈ V
51 fvex 6680 . . . . . . . . . 10 (1st𝑓) ∈ V
5250, 51coex 7623 . . . . . . . . 9 ((1st𝑡) ∘ (1st𝑓)) ∈ V
53 ovex 7181 . . . . . . . . 9 ((2nd𝑡) (2nd𝑓)) ∈ V
5452, 53op1st 7688 . . . . . . . 8 (1st ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((1st𝑡) ∘ (1st𝑓))
5549, 54syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = ((1st𝑡) ∘ (1st𝑓)))
5655fveq2d 6671 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = (𝑠‘((1st𝑡) ∘ (1st𝑓))))
571, 2, 3, 4, 12dvhvsca 38104 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
58573adantr3 1165 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = ⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩)
5958fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
60 fvex 6680 . . . . . . . . 9 (𝑠‘(1st𝑡)) ∈ V
61 vex 3503 . . . . . . . . . 10 𝑠 ∈ V
62 fvex 6680 . . . . . . . . . 10 (2nd𝑡) ∈ V
6361, 62coex 7623 . . . . . . . . 9 (𝑠 ∘ (2nd𝑡)) ∈ V
6460, 63op1st 7688 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠‘(1st𝑡))
6559, 64syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (𝑠‘(1st𝑡)))
661, 2, 3, 4, 12dvhvsca 38104 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
67663adantr2 1164 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
6867fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
69 fvex 6680 . . . . . . . . 9 (𝑠‘(1st𝑓)) ∈ V
70 fvex 6680 . . . . . . . . . 10 (2nd𝑓) ∈ V
7161, 70coex 7623 . . . . . . . . 9 (𝑠 ∘ (2nd𝑓)) ∈ V
7269, 71op1st 7688 . . . . . . . 8 (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠‘(1st𝑓))
7368, 72syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
7465, 73coeq12d 5734 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))) = ((𝑠‘(1st𝑡)) ∘ (𝑠‘(1st𝑓))))
7546, 56, 743eqtr4d 2871 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))))
7630adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
7716adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
7838, 77eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
79 xp2nd 7713 . . . . . . . . . 10 (𝑡 ∈ (𝑇 × 𝐸) → (2nd𝑡) ∈ 𝐸)
8039, 79syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ 𝐸)
8180, 77eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑡) ∈ (Base‘𝐷))
82 xp2nd 7713 . . . . . . . . . 10 (𝑓 ∈ (𝑇 × 𝐸) → (2nd𝑓) ∈ 𝐸)
8342, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
8483, 77eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
8514, 17, 19ringdi 19236 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8676, 78, 81, 84, 85syl13anc 1366 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd𝑡) (2nd𝑓))) = ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))))
8714, 17ringacl 19248 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ (2nd𝑡) ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷)) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8876, 81, 84, 87syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ (Base‘𝐷))
8988, 77eleqtrrd 2921 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd𝑡) (2nd𝑓)) ∈ 𝐸)
901, 2, 3, 4, 10, 19dvhmulr 38089 . . . . . . . 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 38089 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑡) ∈ 𝐸)) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
9337, 38, 80, 92syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑡)) = (𝑠 ∘ (2nd𝑡)))
941, 2, 3, 4, 10, 19dvhmulr 38089 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9537, 38, 83, 94syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd𝑓)) = (𝑠 ∘ (2nd𝑓)))
9693, 95oveq12d 7166 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑡)) (𝑠 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9786, 91, 963eqtr3d 2869 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ ((2nd𝑡) (2nd𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
9848fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩))
9952, 53op2nd 7689 . . . . . . . 8 (2nd ‘⟨((1st𝑡) ∘ (1st𝑓)), ((2nd𝑡) (2nd𝑓))⟩) = ((2nd𝑡) (2nd𝑓))
10098, 99syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = ((2nd𝑡) (2nd𝑓)))
101100coeq2d 5732 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = (𝑠 ∘ ((2nd𝑡) (2nd𝑓))))
10258fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩))
10360, 63op2nd 7689 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑡)), (𝑠 ∘ (2nd𝑡))⟩) = (𝑠 ∘ (2nd𝑡))
104102, 103syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (𝑠 ∘ (2nd𝑡)))
10567fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
10669, 71op2nd 7689 . . . . . . . 8 (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩) = (𝑠 ∘ (2nd𝑓))
107105, 106syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
108104, 107oveq12d 7166 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))) = ((𝑠 ∘ (2nd𝑡)) (𝑠 ∘ (2nd𝑓))))
10997, 101, 1083eqtr4d 2871 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓))))
11075, 109opeq12d 4810 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩ = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
1111, 2, 3, 4, 10, 17, 8dvhvaddcl 38098 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1121113adantr1 1163 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))
1131, 2, 3, 4, 12dvhvsca 38104 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
11437, 38, 112, 113syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ⟨(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))⟩)
115353adantr3 1165 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸))
1161, 2, 3, 4, 12dvhvscacl 38106 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1171163adantr2 1164 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1181, 2, 3, 4, 10, 8, 17dvhvadd 38095 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑡) ∈ (𝑇 × 𝐸) ∧ (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
11937, 115, 117, 118syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) (2nd ‘(𝑠 · 𝑓)))⟩)
120110, 114, 1193eqtr4d 2871 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓)))
121 simpl 483 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
122 simpr1 1188 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠𝐸)
123 simpr2 1189 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡𝐸)
124 simpr3 1190 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸))
125124, 43syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st𝑓) ∈ 𝑇)
126 eqid 2826 . . . . . . . 8 (+g‘((EDRing‘𝐾)‘𝑊)) = (+g‘((EDRing‘𝐾)‘𝑊))
1271, 2, 3, 21, 126erngplus2 37807 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇)) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
128121, 122, 123, 125, 127syl13anc 1366 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
12922fveq2d 6671 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (+g𝐷) = (+g‘((EDRing‘𝐾)‘𝑊)))
13017, 129syl5eq 2873 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑊𝐻) → = (+g‘((EDRing‘𝐾)‘𝑊)))
131130oveqd 7165 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑠 𝑡) = (𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡))
132131fveq1d 6669 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
133132adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st𝑓)))
134663adantr2 1164 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = ⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩)
135134fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
136135, 72syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st𝑓)))
1371, 2, 3, 4, 12dvhvsca 38104 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
1381373adantr1 1163 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩)
139138fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
140 fvex 6680 . . . . . . . . 9 (𝑡‘(1st𝑓)) ∈ V
141 vex 3503 . . . . . . . . . 10 𝑡 ∈ V
142141, 70coex 7623 . . . . . . . . 9 (𝑡 ∘ (2nd𝑓)) ∈ V
143140, 142op1st 7688 . . . . . . . 8 (1st ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡‘(1st𝑓))
144139, 143syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (𝑡‘(1st𝑓)))
145136, 144coeq12d 5734 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))) = ((𝑠‘(1st𝑓)) ∘ (𝑡‘(1st𝑓))))
146128, 133, 1453eqtr4d 2871 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡)‘(1st𝑓)) = ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))))
14730adantr 481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring)
14816adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷))
149122, 148eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷))
150123, 148eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (Base‘𝐷))
151124, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ 𝐸)
152151, 148eleqtrd 2920 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd𝑓) ∈ (Base‘𝐷))
15314, 17, 19ringdir 19237 . . . . . . . 8 ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷) ∧ (2nd𝑓) ∈ (Base‘𝐷))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
154147, 149, 150, 152, 153syl13anc 1366 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) × (2nd𝑓)) = ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))))
15514, 17ringacl 19248 . . . . . . . . . 10 ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷)) → (𝑠 𝑡) ∈ (Base‘𝐷))
156147, 149, 150, 155syl3anc 1365 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ (Base‘𝐷))
157156, 148eleqtrrd 2921 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 𝑡) ∈ 𝐸)
1581, 2, 3, 4, 10, 19dvhmulr 38089 . . . . . . . 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 38089 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸)) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
162121, 123, 151, 161syl12anc 834 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 × (2nd𝑓)) = (𝑡 ∘ (2nd𝑓)))
163160, 162oveq12d 7166 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd𝑓)) (𝑡 × (2nd𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
164154, 159, 1633eqtr3d 2869 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
165134fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘⟨(𝑠‘(1st𝑓)), (𝑠 ∘ (2nd𝑓))⟩))
166165, 106syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd𝑓)))
167138fveq2d 6671 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
168140, 142op2nd 7689 . . . . . . . 8 (2nd ‘⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = (𝑡 ∘ (2nd𝑓))
169167, 168syl6eq 2877 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (𝑡 ∘ (2nd𝑓)))
170166, 169oveq12d 7166 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))) = ((𝑠 ∘ (2nd𝑓)) (𝑡 ∘ (2nd𝑓))))
171164, 170eqtr4d 2864 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) ∘ (2nd𝑓)) = ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓))))
172146, 171opeq12d 4810 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩ = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
1731, 2, 3, 4, 12dvhvsca 38104 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
174121, 157, 124, 173syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ⟨((𝑠 𝑡)‘(1st𝑓)), ((𝑠 𝑡) ∘ (2nd𝑓))⟩)
1751163adantr2 1164 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))
1761, 2, 3, 4, 12dvhvscacl 38106 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1771763adantr1 1163 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))
1781, 2, 3, 4, 10, 8, 17dvhvadd 38095 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠 · 𝑓) ∈ (𝑇 × 𝐸) ∧ (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
179121, 175, 177, 178syl12anc 834 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ⟨((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) (2nd ‘(𝑡 · 𝑓)))⟩)
180172, 174, 1793eqtr4d 2871 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓)))
1811, 2, 3tendocoval 37769 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸) ∧ (1st𝑓) ∈ 𝑇) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
182121, 122, 123, 125, 181syl121anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡)‘(1st𝑓)) = (𝑠‘(𝑡‘(1st𝑓))))
183 coass 6116 . . . . . . 7 ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))
184183a1i 11 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) ∘ (2nd𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd𝑓))))
185182, 184opeq12d 4810 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩ = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
1861, 3tendococl 37775 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑡𝐸) → (𝑠𝑡) ∈ 𝐸)
187121, 122, 123, 186syl3anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠𝑡) ∈ 𝐸)
1881, 2, 3, 4, 12dvhvsca 38104 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑠𝑡) ∈ 𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
189121, 187, 124, 188syl12anc 834 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = ⟨((𝑠𝑡)‘(1st𝑓)), ((𝑠𝑡) ∘ (2nd𝑓))⟩)
1901, 2, 3tendocl 37770 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (1st𝑓) ∈ 𝑇) → (𝑡‘(1st𝑓)) ∈ 𝑇)
191121, 123, 125, 190syl3anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡‘(1st𝑓)) ∈ 𝑇)
1921, 3tendococl 37775 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸 ∧ (2nd𝑓) ∈ 𝐸) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
193121, 123, 151, 192syl3anc 1365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)
1941, 2, 3, 4, 12dvhopvsca 38105 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸 ∧ (𝑡‘(1st𝑓)) ∈ 𝑇 ∧ (𝑡 ∘ (2nd𝑓)) ∈ 𝐸)) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
195121, 122, 191, 193, 194syl13anc 1366 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩) = ⟨(𝑠‘(𝑡‘(1st𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd𝑓)))⟩)
196185, 189, 1953eqtr4d 2871 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠𝑡) · 𝑓) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
1971, 2, 3, 4, 10, 19dvhmulr 38089 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸)) → (𝑠 × 𝑡) = (𝑠𝑡))
1981973adantr3 1165 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × 𝑡) = (𝑠𝑡))
199198oveq1d 7163 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠𝑡) · 𝑓))
200138oveq2d 7164 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · ⟨(𝑡‘(1st𝑓)), (𝑡 ∘ (2nd𝑓))⟩))
201196, 199, 2003eqtr4d 2871 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝑡𝐸𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓)))
202 xp1st 7712 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (1st𝑠) ∈ 𝑇)
203202adantl 482 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (1st𝑠) ∈ 𝑇)
204 fvresi 6931 . . . . . 6 ((1st𝑠) ∈ 𝑇 → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
205203, 204syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇)‘(1st𝑠)) = (1st𝑠))
206 xp2nd 7713 . . . . . . 7 (𝑠 ∈ (𝑇 × 𝐸) → (2nd𝑠) ∈ 𝐸)
2071, 2, 3tendof 37766 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (2nd𝑠) ∈ 𝐸) → (2nd𝑠):𝑇𝑇)
208206, 207sylan2 592 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (2nd𝑠):𝑇𝑇)
209 fcoi2 6550 . . . . . 6 ((2nd𝑠):𝑇𝑇 → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
210208, 209syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∘ (2nd𝑠)) = (2nd𝑠))
211205, 210opeq12d 4810 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩ = ⟨(1st𝑠), (2nd𝑠)⟩)
2121, 2, 3tendoidcl 37772 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
213212anim1i 614 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸)))
2141, 2, 3, 4, 12dvhvsca 38104 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸𝑠 ∈ (𝑇 × 𝐸))) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
215213, 214syldan 591 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = ⟨(( I ↾ 𝑇)‘(1st𝑠)), (( I ↾ 𝑇) ∘ (2nd𝑠))⟩)
216 1st2nd2 7719 . . . . 5 (𝑠 ∈ (𝑇 × 𝐸) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
217216adantl 482 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 𝑠 = ⟨(1st𝑠), (2nd𝑠)⟩)
218211, 215, 2173eqtr4d 2871 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 𝑠)
2197, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218islmodd 19560 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LMod)
22010islvec 19796 . 2 (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing))
221219, 28, 220sylanbrc 583 1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑈 ∈ LVec)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107  cop 4570   I cid 5458   × cxp 5552  cres 5556  ccom 5558  wf 6348  cfv 6352  (class class class)co 7148  1st c1st 7678  2nd c2nd 7679  Basecbs 16473  +gcplusg 16555  .rcmulr 16556  Scalarcsca 16558   ·𝑠 cvsca 16559  0gc0g 16703  invgcminusg 18034  1rcur 19171  Ringcrg 19217  DivRingcdr 19422  LModclmod 19554  LVecclvec 19794  HLchlt 36353  LHypclh 36987  LTrncltrn 37104  TEndoctendo 37755  EDRingcedring 37756  DVecHcdvh 38081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-riotaBAD 35956
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-1st 7680  df-2nd 7681  df-tpos 7883  df-undef 7930  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-sca 16571  df-vsca 16572  df-0g 16705  df-proset 17528  df-poset 17546  df-plt 17558  df-lub 17574  df-glb 17575  df-join 17576  df-meet 17577  df-p0 17639  df-p1 17640  df-lat 17646  df-clat 17708  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-grp 18036  df-minusg 18037  df-mgp 19160  df-ur 19172  df-ring 19219  df-oppr 19293  df-dvdsr 19311  df-unit 19312  df-invr 19342  df-dvr 19353  df-drng 19424  df-lmod 19556  df-lvec 19795  df-oposet 36179  df-ol 36181  df-oml 36182  df-covers 36269  df-ats 36270  df-atl 36301  df-cvlat 36325  df-hlat 36354  df-llines 36501  df-lplanes 36502  df-lvols 36503  df-lines 36504  df-psubsp 36506  df-pmap 36507  df-padd 36799  df-lhyp 36991  df-laut 36992  df-ldil 37107  df-ltrn 37108  df-trl 37162  df-tendo 37758  df-edring 37760  df-dvech 38082
This theorem is referenced by:  dvhlvec  38112
  Copyright terms: Public domain W3C validator