dvhb1dimN

Description: Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvhb1dim.l	⊢ ≤ = ( le ‘ 𝐾 )
	dvhb1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhb1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dvhb1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dvhb1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhb1dim.o	⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	dvhb1dimN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ } = { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ( ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) } )

Proof

Step	Hyp	Ref	Expression
1		dvhb1dim.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dvhb1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dvhb1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dvhb1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		dvhb1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6		dvhb1dim.o	⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7		eqop	⊢ ( 𝑔 ∈ ( 𝑇 × 𝐸 ) → ( 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ ↔ ( ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
8	7	adantl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ ↔ ( ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
9	8	rexbidv	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ ↔ ∃ 𝑠 ∈ 𝐸 ( ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
10		r19.41v	⊢ ( ∃ 𝑠 ∈ 𝐸 ( ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ↔ ( ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) )
11		fvex	⊢ ( 1^st ‘ 𝑔 ) ∈ V
12		eqeq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑔 ) → ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ↔ ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ) )
13	12	rexbidv	⊢ ( 𝑓 = ( 1^st ‘ 𝑔 ) → ( ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) ↔ ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ) )
14	11 13	elab	⊢ ( ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∣ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) } ↔ ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) )
15	1 2 3 4 5	dva1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑓 ∣ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) } = { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } )
16	15	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → { 𝑓 ∣ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) } = { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } )
17	16	eleq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∣ ∃ 𝑠 ∈ 𝐸 𝑓 = ( 𝑠 ‘ 𝐹 ) } ↔ ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } ) )
18	14 17	bitr3id	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ↔ ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } ) )
19		xp1st	⊢ ( 𝑔 ∈ ( 𝑇 × 𝐸 ) → ( 1^st ‘ 𝑔 ) ∈ 𝑇 )
20	19	adantl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( 1^st ‘ 𝑔 ) ∈ 𝑇 )
21		fveq2	⊢ ( 𝑓 = ( 1^st ‘ 𝑔 ) → ( 𝑅 ‘ 𝑓 ) = ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) )
22	21	breq1d	⊢ ( 𝑓 = ( 1^st ‘ 𝑔 ) → ( ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
23	22	elrab3	⊢ ( ( 1^st ‘ 𝑔 ) ∈ 𝑇 → ( ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } ↔ ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
24	20 23	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 1^st ‘ 𝑔 ) ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑅 ‘ 𝐹 ) } ↔ ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
25	18 24	bitrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ↔ ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
26	25	anbi1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( ∃ 𝑠 ∈ 𝐸 ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ↔ ( ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
27	10 26	syl5bb	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ∃ 𝑠 ∈ 𝐸 ( ( 1^st ‘ 𝑔 ) = ( 𝑠 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ↔ ( ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
28	9 27	bitrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ ↔ ( ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) ) )
29	28	rabbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ⟨ ( 𝑠 ‘ 𝐹 ) , 0 ⟩ } = { 𝑔 ∈ ( 𝑇 × 𝐸 ) ∣ ( ( 𝑅 ‘ ( 1^st ‘ 𝑔 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝑔 ) = 0 ) } )

Metamath Proof Explorer

Theorem dvhb1dimN

Proof