Metamath Proof Explorer


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 bitrdi ( 𝑔 = ⟨ 𝑓 , 𝑡 ⟩ → ( 𝑔 = ⟨ ( 𝑠𝐹 ) , 𝑂 ⟩ ↔ ( 𝑓 = ( 𝑠𝐹 ) ∧ 𝑡 = 𝑂 ) ) )
47 46 rexbidv ( 𝑔 = ⟨ 𝑓 , 𝑡 ⟩ → ( ∃ 𝑠𝐸 𝑔 = ⟨ ( 𝑠𝐹 ) , 𝑂 ⟩ ↔ ∃ 𝑠𝐸 ( 𝑓 = ( 𝑠𝐹 ) ∧ 𝑡 = 𝑂 ) ) )
48 47 rabxp { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠𝐸 𝑔 = ⟨ ( 𝑠𝐹 ) , 𝑂 ⟩ } = { ⟨ 𝑓 , 𝑡 ⟩ ∣ ( 𝑓𝑇𝑡𝐸 ∧ ∃ 𝑠𝐸 ( 𝑓 = ( 𝑠𝐹 ) ∧ 𝑡 = 𝑂 ) ) }
49 41 48 eqtr4di ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠𝐸 𝑔 = ⟨ ( 𝑠𝐹 ) , 𝑂 ⟩ } )