This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dicvscacl

Description: Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dicvscacl.l ⊢ ≤ = ( le ‘ 𝐾 )
dicvscacl.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dicvscacl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dicvscacl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dicvscacl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dicvscacl.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dicvscacl.s ⊢ · = ( ·𝑠 ‘ 𝑈 )
Assertion dicvscacl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐼 ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 dicvscacl.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dicvscacl.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 dicvscacl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dicvscacl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 dicvscacl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 dicvscacl.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
7 dicvscacl.s ⊢ · = ( ·𝑠 ‘ 𝑈 )
8 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑋 ∈ 𝐸 )
10 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11 1 2 3 6 5 10 dicssdvh ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
12 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
13 3 12 4 5 10 dvhvbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) )
14 13 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) = ( Base ‘ 𝑈 ) )
15 14 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) = ( Base ‘ 𝑈 ) )
16 11 15 sseqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) )
17 16 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) )
18 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) )
19 17 18 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) )
20 3 12 4 5 7 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ⟩ )
21 8 9 19 20 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ⟩ )
22 fvi ⊢ ( 𝑋 ∈ 𝐸 → ( I ‘ 𝑋 ) = 𝑋 )
23 9 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( I ‘ 𝑋 ) = 𝑋 )
24 23 coeq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) = ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) )
25 24 opeq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ⟩ = ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ⟩ )
26 21 25 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ⟩ )
27 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
28 1 2 3 27 12 6 dicelval1sta ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1st ‘ 𝑌 ) = ( ( 2nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
29 28 3adant3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 1st ‘ 𝑌 ) = ( ( 2nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
30 29 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) = ( 𝑋 ‘ ( ( 2nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
31 1 2 3 4 6 dicelval2nd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 2nd ‘ 𝑌 ) ∈ 𝐸 )
32 31 3adant3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2nd ‘ 𝑌 ) ∈ 𝐸 )
33 3 12 4 tendof ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2nd ‘ 𝑌 ) ∈ 𝐸 ) → ( 2nd ‘ 𝑌 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
34 8 32 33 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2nd ‘ 𝑌 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
35 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
36 1 35 2 3 lhpocnel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
37 36 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
38 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
39 eqid ⊢ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
40 1 2 3 12 39 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
41 8 37 38 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
42 fvco3 ⊢ ( ( ( 2nd ‘ 𝑌 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( 𝑋 ‘ ( ( 2nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
43 34 41 42 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( 𝑋 ‘ ( ( 2nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
44 30 43 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) = ( ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
45 24 fveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
46 44 45 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
47 3 4 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐸 ∧ ( 2nd ‘ 𝑌 ) ∈ 𝐸 ) → ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ∈ 𝐸 )
48 8 9 32 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ∘ ( 2nd ‘ 𝑌 ) ) ∈ 𝐸 )
49 24 48 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ∈ 𝐸 )
50 fvex ⊢ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) ∈ V
51 fvex ⊢ ( I ‘ 𝑋 ) ∈ V
52 fvex ⊢ ( 2nd ‘ 𝑌 ) ∈ V
53 51 52 coex ⊢ ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ∈ V
54 1 2 3 27 12 4 6 50 53 dicopelval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ∈ 𝐸 ) ) )
55 54 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ∈ 𝐸 ) ) )
56 46 49 55 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ⟨ ( 𝑋 ‘ ( 1st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) )
57 26 56 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐼 ‘ 𝑄 ) )