Theorem dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dib1dim.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dib1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dib1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dib1dim.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dib1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		dib1dim.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dib1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dib1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dib1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		dib1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6		dib1dim.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7		dib1dim.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9	1 2 3 4	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
10		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
11	10 2 3 4	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) 𝑊 )
12		eqid	⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13	1 10 2 3 6 12 7	dibval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } ) )
14	8 9 11 13	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } ) )
15		relxp	⊢ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } )
16		opelxp	⊢ ( ⟨ 𝑓 , 𝑡 ⟩ ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) ∧ 𝑡 ∈ { 𝑂 } ) )
17	2 3 4 5 12	dia1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑓 ∣ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) } )
18	17	abeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) ↔ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ) )
19	18	anbi1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) ∧ 𝑡 ∈ { 𝑂 } ) ↔ ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 ∈ { 𝑂 } ) ) )
20	2 3 5	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
21	20	3expa	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
22	21	an32s	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
23	1 2 3 5 6	tendo0cl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
24	23	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → 𝑂 ∈ 𝐸 )
25	22 24	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ 𝑂 ∈ 𝐸 ) )
26		eleq1	⊢ ( 𝑓 = ( 𝑠 ‘ 𝐹 ) → ( 𝑓 ∈ 𝑇 ↔ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ) )
27		eleq1	⊢ ( 𝑡 = 𝑂 → ( 𝑡 ∈ 𝐸 ↔ 𝑂 ∈ 𝐸 ) )
28	26 27	bi2anan9	⊢ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) → ( ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ↔ ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ 𝑂 ∈ 𝐸 ) ) )
29	25 28	syl5ibrcom	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) → ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ) )
30	29	rexlimdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) → ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ) )
31	30	pm4.71rd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) ) )
32		velsn	⊢ ( 𝑡 ∈ { 𝑂 } ↔ 𝑡 = 𝑂 )
33	32	anbi2i	⊢ ( ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 ∈ { 𝑂 } ) ↔ ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) )
34		r19.41v	⊢ ( ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ↔ ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) )
35	33 34	bitr4i	⊢ ( ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 ∈ { 𝑂 } ) ↔ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) )
36		df-3an	⊢ ( ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ) ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) )
37	31 35 36	3bitr4g	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 ∈ { 𝑂 } ) ↔ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) ) )
38	19 37	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) ∧ 𝑡 ∈ { 𝑂 } ) ↔ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) ) )
39	16 38	syl5bb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ⟨ 𝑓 , 𝑡 ⟩ ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } ) ↔ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) ) )
40	15 39	opabbi2dv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) × { 𝑂 } ) = { ⟨ 𝑓 , 𝑡 ⟩ ∣ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) } )
41	14 40	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { ⟨ 𝑓 , 𝑡 ⟩ ∣ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) } )
42		eqeq1	⊢ ( 𝑔 = ⟨ 𝑓 , 𝑡 ⟩ → ( 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ ↔ ⟨ 𝑓 , 𝑡 ⟩ = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ ) )
43		vex	⊢ 𝑓 ∈ V
44		vex	⊢ 𝑡 ∈ V
45	43 44	opth	⊢ ( ⟨ 𝑓 , 𝑡 ⟩ = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ ↔ ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) )
46	42 45	syl6bb	⊢ ( 𝑔 = ⟨ 𝑓 , 𝑡 ⟩ → ( 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ ↔ ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) )
47	46	rexbidv	⊢ ( 𝑔 = ⟨ 𝑓 , 𝑡 ⟩ → ( ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ ↔ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) )
48	47	rabxp	⊢ { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ } = { ⟨ 𝑓 , 𝑡 ⟩ ∣ ( 𝑓 ∈ 𝑇 ∧ 𝑡 ∈ 𝐸 ∧ ∃ 𝑠 ∈ 𝐸 ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑡 = 𝑂 ) ) }
49	41 48	eqtr4di	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑂 ⟩ } )