Theorem dva1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in Crawley p. 120 line 21, but using a non-identity translation (nonzero vector) F whose trace is P rather than P itself; F exists by cdlemf . E is the division ring base by erngdv , and sF is the scalar product by dvavsca . F must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013)

	Ref	Expression
Hypotheses	dva1dim.l	⊢ ≤ = ( le ‘ 𝐾 )
	dva1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dva1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dva1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dva1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dva1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) } = { 𝑔 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) } )

Proof

Step	Hyp	Ref	Expression
1		dva1dim.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dva1dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dva1dim.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dva1dim.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		dva1dim.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6	2 3 5	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
7	1 2 3 4 5	tendotp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
8	6 7	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
9	8	3expb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
10	9	anass1rs	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
11		eleq1	⊢ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( 𝑔 ∈ 𝑇 ↔ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ) )
12		fveq2	⊢ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( 𝑅 ‘ 𝑔 ) = ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) )
13	12	breq1d	⊢ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
14	11 13	anbi12d	⊢ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ↔ ( ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑅 ‘ ( 𝑠 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) )
15	10 14	syl5ibrcom	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) )
16	15	rexlimdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) → ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) )
17		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18		simplr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → 𝐹 ∈ 𝑇 )
19		simprl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → 𝑔 ∈ 𝑇 )
20		simprr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) )
21	1 2 3 4 5	tendoex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ‘ 𝐹 ) = 𝑔 )
22	17 18 19 20 21	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ‘ 𝐹 ) = 𝑔 )
23		eqcom	⊢ ( ( 𝑠 ‘ 𝐹 ) = 𝑔 ↔ 𝑔 = ( 𝑠 ‘ 𝐹 ) )
24	23	rexbii	⊢ ( ∃ 𝑠 ∈ 𝐸 ( 𝑠 ‘ 𝐹 ) = 𝑔 ↔ ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) )
25	22 24	sylib	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) → ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) )
26	25	ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
27	16 26	impbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ) )
28	27	abbidv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) } = { 𝑔 ∣ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) } )
29		df-rab	⊢ { 𝑔 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) } = { 𝑔 ∣ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) ) }
30	28 29	eqtr4di	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∣ ∃ 𝑠 ∈ 𝐸 𝑔 = ( 𝑠 ‘ 𝐹 ) } = { 𝑔 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑔 ) ≤ ( 𝑅 ‘ 𝐹 ) } )