Metamath Proof Explorer


Theorem dicvaddcl

Description: Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014)

Ref Expression
Hypotheses dicvaddcl.l = ( le ‘ 𝐾 )
dicvaddcl.a 𝐴 = ( Atoms ‘ 𝐾 )
dicvaddcl.h 𝐻 = ( LHyp ‘ 𝐾 )
dicvaddcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dicvaddcl.i 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dicvaddcl.p + = ( +g𝑈 )
Assertion dicvaddcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝐼𝑄 ) )

Proof

Step Hyp Ref Expression
1 dicvaddcl.l = ( le ‘ 𝐾 )
2 dicvaddcl.a 𝐴 = ( Atoms ‘ 𝐾 )
3 dicvaddcl.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dicvaddcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dicvaddcl.i 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
6 dicvaddcl.p + = ( +g𝑈 )
7 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9 1 2 3 5 4 8 dicssdvh ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝐼𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
10 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12 3 10 11 4 8 dvhvbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 12 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
14 13 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
15 9 14 sseqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝐼𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
16 15 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝐼𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
17 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → 𝑋 ∈ ( 𝐼𝑄 ) )
18 16 17 sseldd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → 𝑋 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
19 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → 𝑌 ∈ ( 𝐼𝑄 ) )
20 16 19 sseldd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 eqid ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
22 eqid ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
23 3 10 11 4 21 6 22 dvhvadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑋 + 𝑌 ) = ⟨ ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) , ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ⟩ )
24 7 18 20 23 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝑋 + 𝑌 ) = ⟨ ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) , ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ⟩ )
25 1 2 3 11 5 dicelval2nd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑋 ∈ ( 𝐼𝑄 ) ) → ( 2nd𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
26 25 3adant3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 2nd𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 2 3 11 5 dicelval2nd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) → ( 2nd𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
28 27 3adant3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 2nd𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
29 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
30 1 29 2 3 lhpocnel ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) 𝑊 ) )
31 30 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) 𝑊 ) )
32 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
33 eqid ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
34 1 2 3 10 33 ltrniotacl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
35 7 31 32 34 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
36 eqid ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) )
37 10 36 tendospdi2 ( ( ( 2nd𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 2nd𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2nd𝑋 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2nd𝑌 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
38 26 28 35 37 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2nd𝑋 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2nd𝑌 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
39 3 10 11 4 21 36 22 dvhfplusr ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) )
40 39 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) )
41 40 oveqd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) = ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) )
42 41 fveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
43 eqid ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
44 1 2 3 43 10 5 dicelval1sta ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑋 ∈ ( 𝐼𝑄 ) ) → ( 1st𝑋 ) = ( ( 2nd𝑋 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
45 44 3adant3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 1st𝑋 ) = ( ( 2nd𝑋 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
46 1 2 3 43 10 5 dicelval1sta ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) → ( 1st𝑌 ) = ( ( 2nd𝑌 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
47 46 3adant3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 1st𝑌 ) = ( ( 2nd𝑌 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
48 45 47 coeq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) = ( ( ( 2nd𝑋 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2nd𝑌 ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
49 38 42 48 3eqtr4rd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) = ( ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
50 3 10 11 36 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 2nd𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 2nd𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
51 7 26 28 50 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( 2nd𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ) ∘ ( 𝑡 ) ) ) ) ( 2nd𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
52 41 51 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
53 fvex ( 1st𝑋 ) ∈ V
54 fvex ( 1st𝑌 ) ∈ V
55 53 54 coex ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) ∈ V
56 ovex ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ∈ V
57 1 2 3 43 10 11 5 55 56 dicopelval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( ⟨ ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) , ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ⟩ ∈ ( 𝐼𝑄 ) ↔ ( ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) = ( ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
58 57 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( ⟨ ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) , ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ⟩ ∈ ( 𝐼𝑄 ) ↔ ( ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) = ( ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ‘ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
59 49 52 58 mpbir2and ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ⟨ ( ( 1st𝑋 ) ∘ ( 1st𝑌 ) ) , ( ( 2nd𝑋 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 2nd𝑌 ) ) ⟩ ∈ ( 𝐼𝑄 ) )
60 24 59 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼𝑄 ) ∧ 𝑌 ∈ ( 𝐼𝑄 ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝐼𝑄 ) )