lfl1dim2N

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim may be more compatible with lspsn . (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lfl1dim.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lfl1dim.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lfl1dim.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lfl1dim.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
	lfl1dim.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
	lfl1dim.t	⊢ · = ( ._r ‘ 𝐷 )
	lfl1dim.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lfl1dim.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lfl1dim2N	⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∈ 𝐹 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) } )

Proof

Step	Hyp	Ref	Expression
1		lfl1dim.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lfl1dim.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lfl1dim.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lfl1dim.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
5		lfl1dim.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
6		lfl1dim.t	⊢ · = ( ._r ‘ 𝐷 )
7		lfl1dim.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lfl1dim.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	7 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11		eqid	⊢ ( 0_g ‘ 𝐷 ) = ( 0_g ‘ 𝐷 )
12	2 5 11	lmod0cl	⊢ ( 𝑊 ∈ LMod → ( 0_g ‘ 𝐷 ) ∈ 𝐾 )
13	10 12	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝐷 ) ∈ 𝐾 )
14	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( 0_g ‘ 𝐷 ) ∈ 𝐾 )
15		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
16	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → 𝑊 ∈ LMod )
17	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → 𝐺 ∈ 𝐹 )
18	1 2 3 5 6 11 16 17	lfl0sc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
19	15 18	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
20		sneq	⊢ ( 𝑘 = ( 0_g ‘ 𝐷 ) → { 𝑘 } = { ( 0_g ‘ 𝐷 ) } )
21	20	xpeq2d	⊢ ( 𝑘 = ( 0_g ‘ 𝐷 ) → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
22	21	oveq2d	⊢ ( 𝑘 = ( 0_g ‘ 𝐷 ) → ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) = ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
23	22	rspceeqv	⊢ ( ( ( 0_g ‘ 𝐷 ) ∈ 𝐾 ∧ 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) )
24	14 19 23	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) )
25	24	a1d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
26	13	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 0_g ‘ 𝐷 ) ∈ 𝐾 )
27	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LMod )
28		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
29	1 3 4 27 28	lkrssv	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 )
30	10	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑊 ∈ LMod )
31	8	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝐺 ∈ 𝐹 )
32	2 11 1 3 4	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
33	30 31 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
34	33	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
35	34	sseq1d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) ) )
36	35	biimpa	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) )
37	29 36	eqssd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) = 𝑉 )
38	2 11 1 3 4	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
39	27 28 38	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
40	37 39	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
41	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
42	1 2 3 5 6 11 27 41	lfl0sc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
43	40 42	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) )
44	26 43 23	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) )
45	44	ex	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
46		eqid	⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
47	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → 𝑊 ∈ LVec )
48	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → 𝐺 ∈ 𝐹 )
49		simprr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
50	1 2 11 46 3 4	lkrshp	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
51	47 48 49 50	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
52		simplr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → 𝑔 ∈ 𝐹 )
53		simprl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) )
54	1 2 11 46 3 4	lkrshp	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
55	47 52 53 54	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
56	46 47 51 55	lshpcmp	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) )
57	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LVec )
58	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
59		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
60		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) )
61	2 5 6 1 3 4	eqlkr2	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) )
62	57 58 59 60 61	syl121anc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) )
63	62	ex	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
64	56 63	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0_g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
65	25 45 64	pm2.61da2ne	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
66	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LVec )
67	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 )
68		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 )
69	1 2 5 6 3 4 66 67 68	lkrscss	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
70	69	ex	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) ) )
71		fveq2	⊢ ( 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
72	71	sseq2d	⊢ ( 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) ) )
73	72	biimprcd	⊢ ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) → ( 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
74	70 73	syl6	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) )
75	74	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
76	65 75	impbid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) ) )
77	76	rabbidva	⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∈ 𝐹 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘_f · ( 𝑉 × { 𝑘 } ) ) } )

Metamath Proof Explorer

Theorem lfl1dim2N

Proof