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 ‘ 𝐾 ) ‘ 𝑊 ) × 𝐸 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ )
21	8 9 19 20	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ )
22		fvi	⊢ ( 𝑋 ∈ 𝐸 → ( I ‘ 𝑋 ) = 𝑋 )
23	9 22	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( I ‘ 𝑋 ) = 𝑋 )
24	23	coeq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) = ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) )
25	24	opeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ = ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ )
26	21 25	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) = ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ )
27		eqid	⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
28	1 2 3 27 12 6	dicelval1sta	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
29	28	3adant3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
30	29	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) = ( 𝑋 ‘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
31	1 2 3 4 6	dicelval2nd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 2^nd ‘ 𝑌 ) ∈ 𝐸 )
32	31	3adant3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2^nd ‘ 𝑌 ) ∈ 𝐸 )
33	3 12 4	tendof	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) → ( 2^nd ‘ 𝑌 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
34	8 32 33	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2^nd ‘ 𝑌 ) : ( ( 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	⊢ ( ( ( 2^nd ‘ 𝑌 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( 𝑋 ‘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
43	34 41 42	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( 𝑋 ‘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
44	30 43	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) = ( ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
45	24	fveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
46	44 45	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
47	3 4	tendococl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐸 ∧ ( 2^nd ‘ 𝑌 ) ∈ 𝐸 ) → ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ∈ 𝐸 )
48	8 9 32 47	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 ∘ ( 2^nd ‘ 𝑌 ) ) ∈ 𝐸 )
49	24 48	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ∈ 𝐸 )
50		fvex	⊢ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) ∈ V
51		fvex	⊢ ( I ‘ 𝑋 ) ∈ V
52		fvex	⊢ ( 2^nd ‘ 𝑌 ) ∈ V
53	51 52	coex	⊢ ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ∈ V
54	1 2 3 27 12 4 6 50 53	dicopelval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ∈ 𝐸 ) ) )
55	54	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) = ( ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ∈ 𝐸 ) ) )
56	46 49 55	mpbir2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ⟨ ( 𝑋 ‘ ( 1^st ‘ 𝑌 ) ) , ( ( I ‘ 𝑋 ) ∘ ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) )
57	26 56	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐼 ‘ 𝑄 ) )

Metamath Proof Explorer

Theorem dicvscacl

Proof