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

Theorem diblss 37126
Description: The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.)
Hypotheses
Ref Expression
diblss.b 𝐵 = (Base‘𝐾)
diblss.l = (le‘𝐾)
diblss.h 𝐻 = (LHyp‘𝐾)
diblss.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
diblss.i 𝐼 = ((DIsoB‘𝐾)‘𝑊)
diblss.s 𝑆 = (LSubSp‘𝑈)
Assertion
Ref Expression
diblss (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) ∈ 𝑆)

Proof of Theorem diblss
Dummy variables 𝑎 𝑏 𝑥 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2766 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (Scalar‘𝑈) = (Scalar‘𝑈))
2 diblss.h . . . . 5 𝐻 = (LHyp‘𝐾)
3 eqid 2765 . . . . 5 ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
4 diblss.u . . . . 5 𝑈 = ((DVecH‘𝐾)‘𝑊)
5 eqid 2765 . . . . 5 (Scalar‘𝑈) = (Scalar‘𝑈)
6 eqid 2765 . . . . 5 (Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈))
72, 3, 4, 5, 6dvhbase 37039 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊))
87eqcomd 2771 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈)))
98adantr 472 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈)))
10 eqid 2765 . . . . 5 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
11 eqid 2765 . . . . 5 (Base‘𝑈) = (Base‘𝑈)
122, 10, 3, 4, 11dvhvbase 37043 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘𝑈) = (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
1312eqcomd 2771 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈))
1413adantr 472 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈))
15 eqidd 2766 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (+g𝑈) = (+g𝑈))
16 eqidd 2766 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → ( ·𝑠𝑈) = ( ·𝑠𝑈))
17 diblss.s . . 3 𝑆 = (LSubSp‘𝑈)
1817a1i 11 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → 𝑆 = (LSubSp‘𝑈))
19 diblss.b . . . 4 𝐵 = (Base‘𝐾)
20 diblss.l . . . 4 = (le‘𝐾)
21 diblss.i . . . 4 𝐼 = ((DIsoB‘𝐾)‘𝑊)
2219, 20, 2, 21, 4, 11dibss 37125 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) ⊆ (Base‘𝑈))
2322, 14sseqtr4d 3802 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
2419, 20, 2, 21dibn0 37109 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) ≠ ∅)
25 fvex 6388 . . . . . . 7 (𝑥‘(1st𝑎)) ∈ V
26 vex 3353 . . . . . . . 8 𝑥 ∈ V
27 fvex 6388 . . . . . . . 8 (2nd𝑎) ∈ V
2826, 27coex 7316 . . . . . . 7 (𝑥 ∘ (2nd𝑎)) ∈ V
2925, 28op1st 7374 . . . . . 6 (1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) = (𝑥‘(1st𝑎))
3029coeq1i 5450 . . . . 5 ((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)) = ((𝑥‘(1st𝑎)) ∘ (1st𝑏))
31 simpll 783 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
32 simpr1 1248 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊))
33 simplr 785 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑋𝐵𝑋 𝑊))
34 simpr2 1250 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑎 ∈ (𝐼𝑋))
3519, 20, 2, 10, 21dibelval1st1 37106 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑎 ∈ (𝐼𝑋)) → (1st𝑎) ∈ ((LTrn‘𝐾)‘𝑊))
3631, 33, 34, 35syl3anc 1490 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (1st𝑎) ∈ ((LTrn‘𝐾)‘𝑊))
372, 10, 3tendocl 36723 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊))
3831, 32, 36, 37syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊))
39 simpr3 1252 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑏 ∈ (𝐼𝑋))
4019, 20, 2, 10, 21dibelval1st1 37106 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑏 ∈ (𝐼𝑋)) → (1st𝑏) ∈ ((LTrn‘𝐾)‘𝑊))
4131, 33, 39, 40syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (1st𝑏) ∈ ((LTrn‘𝐾)‘𝑊))
422, 10ltrnco 36675 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → ((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ ((LTrn‘𝐾)‘𝑊))
4331, 38, 41, 42syl3anc 1490 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ ((LTrn‘𝐾)‘𝑊))
44 simplll 791 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝐾 ∈ HL)
4544hllatd 35320 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝐾 ∈ Lat)
46 eqid 2765 . . . . . . . . 9 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
4719, 2, 10, 46trlcl 36120 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) ∈ 𝐵)
4831, 43, 47syl2anc 579 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) ∈ 𝐵)
4919, 2, 10, 46trlcl 36120 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) ∈ 𝐵)
5031, 38, 49syl2anc 579 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) ∈ 𝐵)
5119, 2, 10, 46trlcl 36120 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (1st𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st𝑏)) ∈ 𝐵)
5231, 41, 51syl2anc 579 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st𝑏)) ∈ 𝐵)
53 eqid 2765 . . . . . . . . 9 (join‘𝐾) = (join‘𝐾)
5419, 53latjcl 17317 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st𝑏)) ∈ 𝐵) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))) ∈ 𝐵)
5545, 50, 52, 54syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))) ∈ 𝐵)
56 simplrl 795 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑋𝐵)
5720, 53, 2, 10, 46trlco 36683 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))))
5831, 38, 41, 57syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))))
5919, 2, 10, 46trlcl 36120 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (1st𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st𝑎)) ∈ 𝐵)
6031, 36, 59syl2anc 579 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st𝑎)) ∈ 𝐵)
6120, 2, 10, 46, 3tendotp 36717 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) (((trL‘𝐾)‘𝑊)‘(1st𝑎)))
6231, 32, 36, 61syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) (((trL‘𝐾)‘𝑊)‘(1st𝑎)))
63 eqid 2765 . . . . . . . . . . . 12 ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
6419, 20, 2, 63, 21dibelval1st 37105 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑎 ∈ (𝐼𝑋)) → (1st𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
6531, 33, 34, 64syl3anc 1490 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (1st𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
6619, 20, 2, 10, 46, 63diatrl 37000 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (1st𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st𝑎)) 𝑋)
6731, 33, 65, 66syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st𝑎)) 𝑋)
6819, 20, 45, 50, 60, 56, 62, 67lattrd 17324 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) 𝑋)
6919, 20, 2, 63, 21dibelval1st 37105 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑏 ∈ (𝐼𝑋)) → (1st𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
7031, 33, 39, 69syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (1st𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
7119, 20, 2, 10, 46, 63diatrl 37000 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (1st𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st𝑏)) 𝑋)
7231, 33, 70, 71syl3anc 1490 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st𝑏)) 𝑋)
7319, 20, 53latjle12 17328 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st𝑏)) ∈ 𝐵𝑋𝐵)) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st𝑏)) 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))) 𝑋))
7445, 50, 52, 56, 73syl13anc 1491 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎))) 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st𝑏)) 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))) 𝑋))
7568, 72, 74mpbi2and 703 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st𝑏))) 𝑋)
7619, 20, 45, 48, 55, 56, 58, 75lattrd 17324 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) 𝑋)
7719, 20, 2, 10, 46, 63diaelval 36989 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) 𝑋)))
7877adantr 472 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st𝑎)) ∘ (1st𝑏))) 𝑋)))
7943, 76, 78mpbir2and 704 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((𝑥‘(1st𝑎)) ∘ (1st𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
8030, 79syl5eqel 2848 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
81 eqid 2765 . . . . . . . . 9 (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡))))
82 eqid 2765 . . . . . . . . 9 (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
832, 10, 3, 4, 5, 81, 82dvhfplusr 37040 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡)))))
8483ad2antrr 717 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡)))))
8525, 28op2nd 7375 . . . . . . . 8 (2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) = (𝑥 ∘ (2nd𝑎))
86 eqid 2765 . . . . . . . . . . . 12 ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))
8719, 20, 2, 10, 86, 21dibelval2nd 37108 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑎 ∈ (𝐼𝑋)) → (2nd𝑎) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
8831, 33, 34, 87syl3anc 1490 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (2nd𝑎) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
8988coeq2d 5453 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥 ∘ (2nd𝑎)) = (𝑥 ∘ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))))
9019, 2, 10, 3, 86tendo0mulr 36783 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9131, 32, 90syl2anc 579 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥 ∘ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9289, 91eqtrd 2799 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥 ∘ (2nd𝑎)) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9385, 92syl5eq 2811 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9419, 20, 2, 10, 86, 21dibelval2nd 37108 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ 𝑏 ∈ (𝐼𝑋)) → (2nd𝑏) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9531, 33, 39, 94syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (2nd𝑏) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
9684, 93, 95oveq123d 6863 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) = (( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡))))( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))))
97 simpllr 793 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑊𝐻)
9819, 2, 10, 3, 86tendo0cl 36746 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))
9998ad2antrr 717 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))
10019, 2, 10, 3, 86, 81tendo0pl 36747 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) → (( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡))))( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
10144, 97, 99, 100syl21anc 866 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠) ∘ (𝑡))))( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
10296, 101eqtrd 2799 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
103 ovex 6874 . . . . . 6 ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) ∈ V
104103elsn 4349 . . . . 5 (((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) ∈ {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ↔ ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
105102, 104sylibr 225 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) ∈ {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})
106 opelxpi 5314 . . . 4 ((((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏)) ∈ {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) → ⟨((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)), ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏))⟩ ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
10780, 105, 106syl2anc 579 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ⟨((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)), ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏))⟩ ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
10823adantr 472 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝐼𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
109108, 34sseldd 3762 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
110 eqid 2765 . . . . . . 7 ( ·𝑠𝑈) = ( ·𝑠𝑈)
1112, 10, 3, 4, 110dvhvsca 37057 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (𝑥( ·𝑠𝑈)𝑎) = ⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)
11231, 32, 109, 111syl12anc 865 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥( ·𝑠𝑈)𝑎) = ⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)
113112oveq1d 6857 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((𝑥( ·𝑠𝑈)𝑎)(+g𝑈)𝑏) = (⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩(+g𝑈)𝑏))
11488, 99eqeltrd 2844 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (2nd𝑎) ∈ ((TEndo‘𝐾)‘𝑊))
1152, 3tendococl 36728 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (2nd𝑎) ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ (2nd𝑎)) ∈ ((TEndo‘𝐾)‘𝑊))
11631, 32, 114, 115syl3anc 1490 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝑥 ∘ (2nd𝑎)) ∈ ((TEndo‘𝐾)‘𝑊))
117 opelxpi 5314 . . . . . 6 (((𝑥‘(1st𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑥 ∘ (2nd𝑎)) ∈ ((TEndo‘𝐾)‘𝑊)) → ⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
11838, 116, 117syl2anc 579 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
119108, 39sseldd 3762 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
120 eqid 2765 . . . . . 6 (+g𝑈) = (+g𝑈)
1212, 10, 3, 4, 5, 120, 82dvhvadd 37048 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) ∧ 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩(+g𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)), ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏))⟩)
12231, 118, 119, 121syl12anc 865 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩(+g𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)), ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏))⟩)
123113, 122eqtrd 2799 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((𝑥( ·𝑠𝑈)𝑎)(+g𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩) ∘ (1st𝑏)), ((2nd ‘⟨(𝑥‘(1st𝑎)), (𝑥 ∘ (2nd𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd𝑏))⟩)
12419, 20, 2, 10, 86, 63, 21dibval2 37100 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
125124adantr 472 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → (𝐼𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
126107, 123, 1253eltr4d 2859 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼𝑋) ∧ 𝑏 ∈ (𝐼𝑋))) → ((𝑥( ·𝑠𝑈)𝑎)(+g𝑈)𝑏) ∈ (𝐼𝑋))
1271, 9, 14, 15, 16, 18, 23, 24, 126islssd 19205 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wss 3732  {csn 4334  cop 4340   class class class wbr 4809  cmpt 4888   I cid 5184   × cxp 5275  cres 5279  ccom 5281  cfv 6068  (class class class)co 6842  cmpt2 6844  1st c1st 7364  2nd c2nd 7365  Basecbs 16130  +gcplusg 16214  Scalarcsca 16217   ·𝑠 cvsca 16218  lecple 16221  joincjn 17210  Latclat 17311  LSubSpclss 19201  HLchlt 35306  LHypclh 35940  LTrncltrn 36057  trLctrl 36114  TEndoctendo 36708  DIsoAcdia 36984  DVecHcdvh 37034  DIsoBcdib 37094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-riotaBAD 34909
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-undef 7602  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-plusg 16227  df-mulr 16228  df-sca 16230  df-vsca 16231  df-proset 17194  df-poset 17212  df-plt 17224  df-lub 17240  df-glb 17241  df-join 17242  df-meet 17243  df-p0 17305  df-p1 17306  df-lat 17312  df-clat 17374  df-lss 19202  df-oposet 35132  df-ol 35134  df-oml 35135  df-covers 35222  df-ats 35223  df-atl 35254  df-cvlat 35278  df-hlat 35307  df-llines 35454  df-lplanes 35455  df-lvols 35456  df-lines 35457  df-psubsp 35459  df-pmap 35460  df-padd 35752  df-lhyp 35944  df-laut 35945  df-ldil 36060  df-ltrn 36061  df-trl 36115  df-tendo 36711  df-edring 36713  df-disoa 36985  df-dvech 37035  df-dib 37095
This theorem is referenced by:  diblsmopel  37127  cdlemn5pre  37156  cdlemn11c  37165  dihjustlem  37172  dihord1  37174  dihord2a  37175  dihord2b  37176  dihord11c  37180  dihlsscpre  37190  dihopelvalcpre  37204  dihlss  37206  dihord6apre  37212  dihord5b  37215  dihord5apre  37218
  Copyright terms: Public domain W3C validator