Metamath Proof Explorer


Theorem lcfl7N

Description: Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 4-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcfl6.h 𝐻 = ( LHyp ‘ 𝐾 )
lcfl6.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfl6.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfl6.v 𝑉 = ( Base ‘ 𝑈 )
lcfl6.a + = ( +g𝑈 )
lcfl6.t · = ( ·𝑠𝑈 )
lcfl6.s 𝑆 = ( Scalar ‘ 𝑈 )
lcfl6.r 𝑅 = ( Base ‘ 𝑆 )
lcfl6.z 0 = ( 0g𝑈 )
lcfl6.f 𝐹 = ( LFnl ‘ 𝑈 )
lcfl6.l 𝐿 = ( LKer ‘ 𝑈 )
lcfl6.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
lcfl6.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcfl6.g ( 𝜑𝐺𝐹 )
Assertion lcfl7N ( 𝜑 → ( 𝐺𝐶 ↔ ( ( 𝐿𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcfl6.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfl6.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfl6.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfl6.v 𝑉 = ( Base ‘ 𝑈 )
5 lcfl6.a + = ( +g𝑈 )
6 lcfl6.t · = ( ·𝑠𝑈 )
7 lcfl6.s 𝑆 = ( Scalar ‘ 𝑈 )
8 lcfl6.r 𝑅 = ( Base ‘ 𝑆 )
9 lcfl6.z 0 = ( 0g𝑈 )
10 lcfl6.f 𝐹 = ( LFnl ‘ 𝑈 )
11 lcfl6.l 𝐿 = ( LKer ‘ 𝑈 )
12 lcfl6.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
13 lcfl6.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 lcfl6.g ( 𝜑𝐺𝐹 )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lcfl6 ( 𝜑 → ( 𝐺𝐶 ↔ ( ( 𝐿𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
16 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
17 eqid ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
18 eqid ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
19 simplrl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
20 simplrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
21 simprl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
22 eqeq1 ( 𝑣 = 𝑢 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
23 22 rexbidv ( 𝑣 = 𝑢 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
24 23 riotabidv ( 𝑣 = 𝑢 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
25 oveq1 ( 𝑘 = 𝑙 → ( 𝑘 · 𝑥 ) = ( 𝑙 · 𝑥 ) )
26 25 oveq2d ( 𝑘 = 𝑙 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑤 + ( 𝑙 · 𝑥 ) ) )
27 26 eqeq2d ( 𝑘 = 𝑙 → ( 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ) )
28 27 rexbidv ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ) )
29 oveq1 ( 𝑤 = 𝑧 → ( 𝑤 + ( 𝑙 · 𝑥 ) ) = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
30 29 eqeq2d ( 𝑤 = 𝑧 → ( 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
31 30 cbvrexvw ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
32 28 31 bitrdi ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
33 32 cbvriotavw ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
34 24 33 eqtrdi ( 𝑣 = 𝑢 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
35 34 cbvmptv ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
36 21 35 eqtrdi ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) )
37 simprr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
38 eqeq1 ( 𝑣 = 𝑢 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
39 38 rexbidv ( 𝑣 = 𝑢 → ( ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
40 39 riotabidv ( 𝑣 = 𝑢 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
41 oveq1 ( 𝑘 = 𝑙 → ( 𝑘 · 𝑦 ) = ( 𝑙 · 𝑦 ) )
42 41 oveq2d ( 𝑘 = 𝑙 → ( 𝑤 + ( 𝑘 · 𝑦 ) ) = ( 𝑤 + ( 𝑙 · 𝑦 ) ) )
43 42 eqeq2d ( 𝑘 = 𝑙 → ( 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ) )
44 43 rexbidv ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ) )
45 oveq1 ( 𝑤 = 𝑧 → ( 𝑤 + ( 𝑙 · 𝑦 ) ) = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
46 45 eqeq2d ( 𝑤 = 𝑧 → ( 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
47 46 cbvrexvw ( ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ↔ ∃ 𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
48 44 47 bitrdi ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
49 48 cbvriotavw ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
50 40 49 eqtrdi ( 𝑣 = 𝑢 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
51 50 cbvmptv ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
52 37 51 eqtrdi ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
53 36 52 eqtr3d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) = ( 𝑢𝑉 ↦ ( 𝑙𝑅𝑧 ∈ ( ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
54 1 2 3 4 5 6 7 8 9 10 11 16 17 18 19 20 53 lcfl7lem ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑥 = 𝑦 )
55 54 ex ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) → ( ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) )
56 55 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) )
57 56 a1d ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) )
58 57 ancld ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) ) )
59 sneq ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
60 59 fveq2d ( 𝑥 = 𝑦 → ( ‘ { 𝑥 } ) = ( ‘ { 𝑦 } ) )
61 oveq2 ( 𝑥 = 𝑦 → ( 𝑘 · 𝑥 ) = ( 𝑘 · 𝑦 ) )
62 61 oveq2d ( 𝑥 = 𝑦 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑤 + ( 𝑘 · 𝑦 ) ) )
63 62 eqeq2d ( 𝑥 = 𝑦 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
64 60 63 rexeqbidv ( 𝑥 = 𝑦 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
65 64 riotabidv ( 𝑥 = 𝑦 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
66 65 mpteq2dv ( 𝑥 = 𝑦 → ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
67 66 eqeq2d ( 𝑥 = 𝑦 → ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) )
68 67 reu4 ( ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) )
69 58 68 syl6ibr ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
70 reurex ( ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
71 69 70 impbid1 ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
72 71 orbi2d ( 𝜑 → ( ( ( 𝐿𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ↔ ( ( 𝐿𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
73 15 72 bitrd ( 𝜑 → ( 𝐺𝐶 ↔ ( ( 𝐿𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )