diblss

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)

	Ref	Expression
Hypotheses	diblss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	diblss.l	⊢ ≤ = ( le ‘ 𝐾 )
	diblss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	diblss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	diblss.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
	diblss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion	diblss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		diblss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		diblss.l	⊢ ≤ = ( le ‘ 𝐾 )
3		diblss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		diblss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		diblss.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
6		diblss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
7		eqidd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 ) )
8		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
9		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
10		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
11	3 8 4 9 10	dvhbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
12	11	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
14		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
15		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
16	3 14 8 4 15	dvhvbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
17	16	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
18	17	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
19		eqidd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( +_g ‘ 𝑈 ) = ( +_g ‘ 𝑈 ) )
20		eqidd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ·_𝑠 ‘ 𝑈 ) = ( ·_𝑠 ‘ 𝑈 ) )
21	6	a1i	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑆 = ( LSubSp ‘ 𝑈 ) )
22	1 2 3 5 4 15	dibss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) )
23	22 18	sseqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
24	1 2 3 5	dibn0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ≠ ∅ )
25		fvex	⊢ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ V
26		vex	⊢ 𝑥 ∈ V
27		fvex	⊢ ( 2^nd ‘ 𝑎 ) ∈ V
28	26 27	coex	⊢ ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ∈ V
29	25 28	op1st	⊢ ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) = ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) )
30	29	coeq1i	⊢ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) = ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) )
31		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32		simpr1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
33		simplr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
34		simpr2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) )
35	1 2 3 14 5	dibelval1st1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 1^st ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
36	31 33 34 35	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
37	3 14 8	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 1^st ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
38	31 32 36 37	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
39		simpr3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) )
40	1 2 3 14 5	dibelval1st1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 1^st ‘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
41	31 33 39 40	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
42	3 14	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 1^st ‘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
43	31 38 41 42	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
44		simplll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝐾 ∈ HL )
45	44	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝐾 ∈ Lat )
46		eqid	⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
47	1 3 14 46	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ∈ 𝐵 )
48	31 43 47	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ∈ 𝐵 )
49	1 3 14 46	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ∈ 𝐵 )
50	31 38 49	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ∈ 𝐵 )
51	1 3 14 46	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ∈ 𝐵 )
52	31 41 51	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ∈ 𝐵 )
53		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
54	1 53	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ∈ 𝐵 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ∈ 𝐵 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) ∈ 𝐵 )
55	45 50 52 54	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) ∈ 𝐵 )
56		simplrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
57	2 53 3 14 46	trlco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 1^st ‘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ≤ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) )
58	31 38 41 57	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ≤ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) )
59	1 3 14 46	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) ∈ 𝐵 )
60	31 36 59	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) ∈ 𝐵 )
61	2 3 14 46 8	tendotp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 1^st ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) )
62	31 32 36 61	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) )
63		eqid	⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
64	1 2 3 63 5	dibelval1st	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 1^st ‘ 𝑎 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
65	31 33 34 64	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝑎 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
66	1 2 3 14 46 63	diatrl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 1^st ‘ 𝑎 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) ≤ 𝑋 )
67	31 33 65 66	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑎 ) ) ≤ 𝑋 )
68	1 2 45 50 60 56 62 67	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ≤ 𝑋 )
69	1 2 3 63 5	dibelval1st	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 1^st ‘ 𝑏 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
70	31 33 39 69	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝑏 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
71	1 2 3 14 46 63	diatrl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 1^st ‘ 𝑏 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ≤ 𝑋 )
72	31 33 70 71	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ≤ 𝑋 )
73	1 2 53	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ∈ 𝐵 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ≤ 𝑋 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ≤ 𝑋 ) ↔ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 ) )
74	45 50 52 56 73	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ≤ 𝑋 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ≤ 𝑋 ) ↔ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 ) )
75	68 72 74	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 )
76	1 2 45 48 55 56 58 75	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 )
77	1 2 3 14 46 63	diaelval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ↔ ( ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 ) ) )
78	77	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ↔ ( ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ) ≤ 𝑋 ) ) )
79	43 76 78	mpbir2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
80	30 79	eqeltrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
81		eqid	⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) )
82		eqid	⊢ ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( +_g ‘ ( Scalar ‘ 𝑈 ) )
83	3 14 8 4 9 81 82	dvhfplusr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) )
84	83	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) )
85	25 28	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) = ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) )
86		eqid	⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) )
87	1 2 3 14 86 5	dibelval2nd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 2^nd ‘ 𝑎 ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
88	31 33 34 87	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 2^nd ‘ 𝑎 ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
89	88	coeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) = ( 𝑥 ∘ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) )
90	1 3 14 8 86	tendo0mulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∘ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
91	31 32 90	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ∘ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
92	89 91	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
93	85 92	syl5eq	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
94	1 2 3 14 86 5	dibelval2nd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 2^nd ‘ 𝑏 ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
95	31 33 39 94	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 2^nd ‘ 𝑏 ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
96	84 93 95	oveq123d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) = ( ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) )
97		simpllr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑊 ∈ 𝐻 )
98	1 3 14 8 86	tendo0cl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
99	98	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
100	1 3 14 8 86 81	tendo0pl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
101	44 97 99 100	syl21anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
102	96 101	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
103		ovex	⊢ ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ∈ V
104	103	elsn	⊢ ( ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ∈ { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ↔ ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) )
105	102 104	sylibr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ∈ { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } )
106		opelxpi	⊢ ( ( ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ∈ { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ) → ⟨ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ⟩ ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ) )
107	80 105 106	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ⟨ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ⟩ ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ) )
108	23	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
109	108 34	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑎 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
110		eqid	⊢ ( ·_𝑠 ‘ 𝑈 ) = ( ·_𝑠 ‘ 𝑈 )
111	3 14 8 4 110	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑥 ( ·_𝑠 ‘ 𝑈 ) 𝑎 ) = ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ )
112	31 32 109 111	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ( ·_𝑠 ‘ 𝑈 ) 𝑎 ) = ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ )
113	112	oveq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·_𝑠 ‘ 𝑈 ) 𝑎 ) ( +_g ‘ 𝑈 ) 𝑏 ) = ( ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ( +_g ‘ 𝑈 ) 𝑏 ) )
114	88 99	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 2^nd ‘ 𝑎 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
115	3 8	tendococl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 2^nd ‘ 𝑎 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
116	31 32 114 115	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
117		opelxpi	⊢ ( ( ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
118	38 116 117	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
119	108 39	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑏 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
120		eqid	⊢ ( +_g ‘ 𝑈 ) = ( +_g ‘ 𝑈 )
121	3 14 8 4 9 120 82	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑏 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ( +_g ‘ 𝑈 ) 𝑏 ) = ⟨ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ⟩ )
122	31 118 119 121	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ( +_g ‘ 𝑈 ) 𝑏 ) = ⟨ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ⟩ )
123	113 122	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·_𝑠 ‘ 𝑈 ) 𝑎 ) ( +_g ‘ 𝑈 ) 𝑏 ) = ⟨ ( ( 1^st ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ∘ ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ ⟨ ( 𝑥 ‘ ( 1^st ‘ 𝑎 ) ) , ( 𝑥 ∘ ( 2^nd ‘ 𝑎 ) ) ⟩ ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑏 ) ) ⟩ )
124	1 2 3 14 86 63 5	dibval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ) )
125	124	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) } ) )
126	107 123 125	3eltr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·_𝑠 ‘ 𝑈 ) 𝑎 ) ( +_g ‘ 𝑈 ) 𝑏 ) ∈ ( 𝐼 ‘ 𝑋 ) )
127	7 13 18 19 20 21 23 24 126	islssd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )

Metamath Proof Explorer

Theorem diblss

Proof