Theorem diblss 41152

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.

Step	Hyp	Ref	Expression
1		eqidd 2735	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (Scalar‘𝑈) = (Scalar‘𝑈))
2		diblss.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3		eqid 2734	. . . . 5 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
4		diblss.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		eqid 2734	. . . . 5 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
6		eqid 2734	. . . . 5 ⊢ (Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈))
7	2, 3, 4, 5, 6	dvhbase 41065	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊))
8	7	eqcomd 2740	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈)))
9	8	adantr 480	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈)))
10		eqid 2734	. . . . 5 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
11		eqid 2734	. . . . 5 ⊢ (Base‘𝑈) = (Base‘𝑈)
12	2, 10, 3, 4, 11	dvhvbase 41069	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
13	12	eqcomd 2740	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈))
14	13	adantr 480	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈))
15		eqidd 2735	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (+g‘𝑈) = (+g‘𝑈))
16		eqidd 2735	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ( ·𝑠 ‘𝑈) = ( ·𝑠 ‘𝑈))
17		diblss.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑈)
18	17	a1i 11	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑆 = (LSubSp‘𝑈))
19		diblss.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
20		diblss.l	. . . 4 ⊢ ≤ = (le‘𝐾)
21		diblss.i	. . . 4 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
22	19, 20, 2, 21, 4, 11	dibss 41151	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ (Base‘𝑈))
23	22, 14	sseqtrrd 4036	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
24	19, 20, 2, 21	dibn0 41135	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅)
25		fvex 6919	. . . . . . 7 ⊢ (𝑥‘(1st ‘𝑎)) ∈ V
26		vex 3481	. . . . . . . 8 ⊢ 𝑥 ∈ V
27		fvex 6919	. . . . . . . 8 ⊢ (2nd ‘𝑎) ∈ V
28	26, 27	coex 7952	. . . . . . 7 ⊢ (𝑥 ∘ (2nd ‘𝑎)) ∈ V
29	25, 28	op1st 8020	. . . . . 6 ⊢ (1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) = (𝑥‘(1st ‘𝑎))
30	29	coeq1i 5872	. . . . 5 ⊢ ((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)) = ((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))
31		simpll 767	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
32		simpr1 1193	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊))
33		simplr 769	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))
34		simpr2 1194	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑎 ∈ (𝐼‘𝑋))
35	19, 20, 2, 10, 21	dibelval1st1 41132	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊))
36	31, 33, 34, 35	syl3anc 1370	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊))
37	2, 10, 3	tendocl 40749	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊))
38	31, 32, 36, 37	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊))
39		simpr3 1195	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑏 ∈ (𝐼‘𝑋))
40	19, 20, 2, 10, 21	dibelval1st1 41132	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊))
41	31, 33, 39, 40	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊))
42	2, 10	ltrnco 40701	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → ((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ ((LTrn‘𝐾)‘𝑊))
43	31, 38, 41, 42	syl3anc 1370	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ ((LTrn‘𝐾)‘𝑊))
44		simplll 775	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝐾 ∈ HL)
45	44	hllatd 39345	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝐾 ∈ Lat)
46		eqid 2734	. . . . . . . . 9 ⊢ ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
47	19, 2, 10, 46	trlcl 40146	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ∈ 𝐵)
48	31, 43, 47	syl2anc 584	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ∈ 𝐵)
49	19, 2, 10, 46	trlcl 40146	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵)
50	31, 38, 49	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵)
51	19, 2, 10, 46	trlcl 40146	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵)
52	31, 41, 51	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵)
53		eqid 2734	. . . . . . . . 9 ⊢ (join‘𝐾) = (join‘𝐾)
54	19, 53	latjcl 18496	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ∈ 𝐵)
55	45, 50, 52, 54	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ∈ 𝐵)
56		simplrl 777	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑋 ∈ 𝐵)
57	20, 53, 2, 10, 46	trlco 40709	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ≤ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))))
58	31, 38, 41, 57	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ≤ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))))
59	19, 2, 10, 46	trlcl 40146	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ∈ 𝐵)
60	31, 36, 59	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ∈ 𝐵)
61	20, 2, 10, 46, 3	tendotp 40743	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)))
62	31, 32, 36, 61	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)))
63		eqid 2734	. . . . . . . . . . . 12 ⊢ ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
64	19, 20, 2, 63, 21	dibelval1st 41131	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
65	31, 33, 34, 64	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
66	19, 20, 2, 10, 46, 63	diatrl 41026	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ≤ 𝑋)
67	31, 33, 65, 66	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ≤ 𝑋)
68	19, 20, 45, 50, 60, 56, 62, 67	lattrd 18503	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋)
69	19, 20, 2, 63, 21	dibelval1st 41131	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
70	31, 33, 39, 69	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
71	19, 20, 2, 10, 46, 63	diatrl 41026	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋)
72	31, 33, 70, 71	syl3anc 1370	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋)
73	19, 20, 53	latjle12 18507	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋))
74	45, 50, 52, 56, 73	syl13anc 1371	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋))
75	68, 72, 74	mpbi2and 712	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋)
76	19, 20, 45, 48, 55, 56, 58, 75	lattrd 18503	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ≤ 𝑋)
77	19, 20, 2, 10, 46, 63	diaelval 41015	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ≤ 𝑋)))
78	77	adantr 480	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏))) ≤ 𝑋)))
79	43, 76, 78	mpbir2and 713	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥‘(1st ‘𝑎)) ∘ (1st ‘𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
80	30, 79	eqeltrid 2842	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋))
81		eqid 2734	. . . . . . . . 9 ⊢ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))
82		eqid 2734	. . . . . . . . 9 ⊢ (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
83	2, 10, 3, 4, 5, 81, 82	dvhfplusr 41066	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ)))))
84	83	ad2antrr 726	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ)))))
85	25, 28	op2nd 8021	. . . . . . . 8 ⊢ (2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) = (𝑥 ∘ (2nd ‘𝑎))
86		eqid 2734	. . . . . . . . . . . 12 ⊢ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))
87	19, 20, 2, 10, 86, 21	dibelval2nd 41134	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (2nd ‘𝑎) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
88	31, 33, 34, 87	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑎) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
89	88	coeq2d 5875	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) = (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))))
90	19, 2, 10, 3, 86	tendo0mulr 40809	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
91	31, 32, 90	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
92	89, 91	eqtrd 2774	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
93	85, 92	eqtrid 2786	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
94	19, 20, 2, 10, 86, 21	dibelval2nd 41134	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (2nd ‘𝑏) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
95	31, 33, 39, 94	syl3anc 1370	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑏) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
96	84, 93, 95	oveq123d 7451	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))))
97		simpllr 776	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑊 ∈ 𝐻)
98	19, 2, 10, 3, 86	tendo0cl 40772	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))
99	98	ad2antrr 726	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))
100	19, 2, 10, 3, 86, 81	tendo0pl 40773	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) → ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
101	44, 97, 99, 100	syl21anc 838	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
102	96, 101	eqtrd 2774	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
103		ovex 7463	. . . . . 6 ⊢ ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ V
104	103	elsn 4645	. . . . 5 ⊢ (((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ↔ ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))
105	102, 104	sylibr 234	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})
106		opelxpi 5725	. . . 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 ↾ 𝐵))}))
107	80, 105, 106	syl2anc 584	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ⟨((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)), ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))⟩ ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
108	23	adantr 480	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐼‘𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
109	108, 34	sseldd 3995	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
110		eqid 2734	. . . . . . 7 ⊢ ( ·𝑠 ‘𝑈) = ( ·𝑠 ‘𝑈)
111	2, 10, 3, 4, 110	dvhvsca 41083	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (𝑥( ·𝑠 ‘𝑈)𝑎) = ⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)
112	31, 32, 109, 111	syl12anc 837	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥( ·𝑠 ‘𝑈)𝑎) = ⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)
113	112	oveq1d 7445	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠 ‘𝑈)𝑎)(+g‘𝑈)𝑏) = (⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩(+g‘𝑈)𝑏))
114	88, 99	eqeltrd 2838	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑎) ∈ ((TEndo‘𝐾)‘𝑊))
115	2, 3	tendococl 40754	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (2nd ‘𝑎) ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊))
116	31, 32, 114, 115	syl3anc 1370	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊))
117		opelxpi 5725	. . . . . 6 ⊢ (((𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊)) → ⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
118	38, 116, 117	syl2anc 584	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
119	108, 39	sseldd 3995	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
120		eqid 2734	. . . . . 6 ⊢ (+g‘𝑈) = (+g‘𝑈)
121	2, 10, 3, 4, 5, 120, 82	dvhvadd 41074	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) ∧ 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩(+g‘𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)), ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))⟩)
122	31, 118, 119, 121	syl12anc 837	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩(+g‘𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)), ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))⟩)
123	113, 122	eqtrd 2774	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠 ‘𝑈)𝑎)(+g‘𝑈)𝑏) = ⟨((1st ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩) ∘ (1st ‘𝑏)), ((2nd ‘⟨(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))⟩)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))⟩)
124	19, 20, 2, 10, 86, 63, 21	dibval2 41126	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
125	124	adantr 480	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}))
126	107, 123, 125	3eltr4d 2853	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠 ‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ (𝐼‘𝑋))
127	1, 9, 14, 15, 16, 18, 23, 24, 126	islssd 20950	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ⊆ wss 3962  {csn 4630  ⟨cop 4636   class class class wbr 5147   ↦ cmpt 5230   I cid 5581   × cxp 5686   ↾ cres 5690   ∘ ccom 5692  ‘cfv 6562  (class class class)co 7430   ∈ cmpo 7432  1^st c1st 8010  2^nd c2nd 8011  Basecbs 17244  +_gcplusg 17297  Scalarcsca 17300   ·_𝑠 cvsca 17301  lecple 17304  joincjn 18368  Latclat 18488  LSubSpclss 20946  HLchlt 39331  LHypclh 39966  LTrncltrn 40083  trLctrl 40140  TEndoctendo 40734  DIsoAcdia 41010  DVecHcdvh 41060  DIsoBcdib 41120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-riotaBAD 38934

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-undef 8296  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-struct 17180  df-slot 17215  df-ndx 17227  df-base 17245  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-proset 18351  df-poset 18370  df-plt 18387  df-lub 18403  df-glb 18404  df-join 18405  df-meet 18406  df-p0 18482  df-p1 18483  df-lat 18489  df-clat 18556  df-lss 20947  df-oposet 39157  df-ol 39159  df-oml 39160  df-covers 39247  df-ats 39248  df-atl 39279  df-cvlat 39303  df-hlat 39332  df-llines 39480  df-lplanes 39481  df-lvols 39482  df-lines 39483  df-psubsp 39485  df-pmap 39486  df-padd 39778  df-lhyp 39970  df-laut 39971  df-ldil 40086  df-ltrn 40087  df-trl 40141  df-tendo 40737  df-edring 40739  df-disoa 41011  df-dvech 41061  df-dib 41121

This theorem is referenced by:  diblsmopel  41153  cdlemn5pre  41182  cdlemn11c  41191  dihjustlem  41198  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord11c  41206  dihlsscpre  41216  dihopelvalcpre  41230  dihlss  41232  dihord6apre  41238  dihord5b  41241  dihord5apre  41244