Metamath Proof Explorer

Theorem lindsunlem

Description: Lemma for lindsun . (Contributed by Thierry Arnoux, 9-May-2023)

Ref Expression
Hypotheses lindsun.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lindsun.0 ⊢ 0 = ( 0g ‘ 𝑊 )
lindsun.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lindsun.u ⊢ ( 𝜑 → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
lindsun.v ⊢ ( 𝜑 → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
lindsun.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
lindsunlem.o ⊢ 𝑂 = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
lindsunlem.f ⊢ 𝐹 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
lindsunlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
lindsunlem.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐹 ∖ { 𝑂 } ) )
lindsunlem.1 ⊢ ( 𝜑 → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) ) )
Assertion lindsunlem ( 𝜑 → ⊥ )

Proof

Step Hyp Ref Expression
1 lindsun.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
2 lindsun.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 lindsun.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
4 lindsun.u ⊢ ( 𝜑 → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
5 lindsun.v ⊢ ( 𝜑 → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
6 lindsun.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
7 lindsunlem.o ⊢ 𝑂 = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
8 lindsunlem.f ⊢ 𝐹 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
9 lindsunlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
10 lindsunlem.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐹 ∖ { 𝑂 } ) )
11 lindsunlem.1 ⊢ ( 𝜑 → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) ) )
12 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) )
13 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14 3 13 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
15 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
16 14 15 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
17 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑊 ∈ Grp )
18 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
19 14 18 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
20 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑊 ∈ Abel )
21 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
22 21 linds1 ⊢ ( 𝑈 ∈ ( LIndS ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
23 4 22 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
24 21 1 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) )
25 14 23 24 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) )
26 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑁 ‘ 𝑈 ) ⊆ ( Base ‘ 𝑊 ) )
27 difssd ⊢ ( 𝜑 → ( 𝑈 ∖ { 𝐶 } ) ⊆ 𝑈 )
28 21 1 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ∖ { 𝐶 } ) ⊆ 𝑈 ) → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ⊆ ( 𝑁 ‘ 𝑈 ) )
29 14 23 27 28 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ⊆ ( 𝑁 ‘ 𝑈 ) )
30 29 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ⊆ ( 𝑁 ‘ 𝑈 ) )
31 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) )
32 30 31 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑥 ∈ ( 𝑁 ‘ 𝑈 ) )
33 26 32 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
34 21 linds1 ⊢ ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
35 5 34 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
36 21 1 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
37 14 35 36 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
38 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
39 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) )
40 38 39 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
41 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
42 21 41 ablcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) )
43 20 33 40 42 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) )
44 12 43 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) = ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) )
45 10 eldifad ⊢ ( 𝜑 → 𝐾 ∈ 𝐹 )
46 23 9 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝑊 ) )
47 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
48 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
49 21 47 48 8 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐾 ∈ 𝐹 ∧ 𝐶 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) )
50 14 45 46 49 syl3anc ⊢ ( 𝜑 → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) )
51 50 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) )
52 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
53 21 41 52 grpsubadd ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) = 𝑦 ↔ ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) = ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ) )
54 53 biimpar ⊢ ( ( ( 𝑊 ∈ Grp ∧ ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) = ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) = 𝑦 )
55 54 an32s ⊢ ( ( ( 𝑊 ∈ Grp ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) = ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ) ∧ ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) = 𝑦 )
56 17 44 51 33 40 55 syl23anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) = 𝑦 )
57 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑊 ∈ LMod )
58 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
59 21 58 1 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) )
60 14 23 59 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) )
61 60 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) )
62 45 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝐾 ∈ 𝐹 )
63 21 1 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
64 14 23 63 syl2anc ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )
65 64 9 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑁 ‘ 𝑈 ) )
66 65 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝐶 ∈ ( 𝑁 ‘ 𝑈 ) )
67 47 48 8 58 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐹 ∧ 𝐶 ∈ ( 𝑁 ‘ 𝑈 ) ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ 𝑈 ) )
68 57 61 62 66 67 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ 𝑈 ) )
69 52 58 lssvsubcl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑈 ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ 𝑈 ) ∧ 𝑥 ∈ ( 𝑁 ‘ 𝑈 ) ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) ∈ ( 𝑁 ‘ 𝑈 ) )
70 57 61 68 32 69 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ( -g ‘ 𝑊 ) 𝑥 ) ∈ ( 𝑁 ‘ 𝑈 ) )
71 56 70 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 ∈ ( 𝑁 ‘ 𝑈 ) )
72 71 39 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 ∈ ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) )
73 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
74 72 73 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 ∈ { 0 } )
75 elsni ⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
76 74 75 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑦 = 0 )
77 76 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑊 ) 0 ) )
78 21 41 2 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 0 ) = 𝑥 )
79 17 33 78 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 0 ) = 𝑥 )
80 12 77 79 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = 𝑥 )
81 80 31 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) )
82 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝐶 ∈ 𝑈 )
83 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝐾 ∈ ( 𝐹 ∖ { 𝑂 } ) )
84 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑊 ∈ LVec )
85 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
86 21 48 1 47 8 7 islinds2 ⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑐 ∈ 𝑈 ∀ 𝑘 ∈ ( 𝐹 ∖ { 𝑂 } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) ) ) )
87 86 simplbda ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LIndS ‘ 𝑊 ) ) → ∀ 𝑐 ∈ 𝑈 ∀ 𝑘 ∈ ( 𝐹 ∖ { 𝑂 } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) )
88 84 85 87 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ∀ 𝑐 ∈ 𝑈 ∀ 𝑘 ∈ ( 𝐹 ∖ { 𝑂 } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) )
89 oveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) )
90 sneq ⊢ ( 𝑐 = 𝐶 → { 𝑐 } = { 𝐶 } )
91 90 difeq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑈 ∖ { 𝑐 } ) = ( 𝑈 ∖ { 𝐶 } ) )
92 91 fveq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) = ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) )
93 89 92 eleq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) )
94 93 notbid ⊢ ( 𝑐 = 𝐶 → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) )
95 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) )
96 95 eleq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ↔ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) )
97 96 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ↔ ¬ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) )
98 94 97 rspc2va ⊢ ( ( ( 𝐶 ∈ 𝑈 ∧ 𝐾 ∈ ( 𝐹 ∖ { 𝑂 } ) ) ∧ ∀ 𝑐 ∈ 𝑈 ∀ 𝑘 ∈ ( 𝐹 ∖ { 𝑂 } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝑐 } ) ) ) → ¬ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) )
99 82 83 88 98 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ¬ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) )
100 81 99 pm2.21fal ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ) ∧ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) → ⊥ )
101 23 ssdifssd ⊢ ( 𝜑 → ( 𝑈 ∖ { 𝐶 } ) ⊆ ( Base ‘ 𝑊 ) )
102 21 58 1 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∖ { 𝐶 } ) ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
103 14 101 102 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
104 58 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝑊 ) )
105 14 103 104 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝑊 ) )
106 21 58 1 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑉 ) ∈ ( LSubSp ‘ 𝑊 ) )
107 14 35 106 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑉 ) ∈ ( LSubSp ‘ 𝑊 ) )
108 58 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝑉 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑊 ) )
109 14 107 108 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑊 ) )
110 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
111 21 1 110 lsmsp2 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ∖ { 𝐶 } ) ⊆ ( Base ‘ 𝑊 ) ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) = ( 𝑁 ‘ ( ( 𝑈 ∖ { 𝐶 } ) ∪ 𝑉 ) ) )
112 14 101 35 111 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) = ( 𝑁 ‘ ( ( 𝑈 ∖ { 𝐶 } ) ∪ 𝑉 ) ) )
113 65 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ( 𝑁 ‘ 𝑈 ) )
114 21 1 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → 𝑉 ⊆ ( 𝑁 ‘ 𝑉 ) )
115 14 35 114 syl2anc ⊢ ( 𝜑 → 𝑉 ⊆ ( 𝑁 ‘ 𝑉 ) )
116 115 sselda ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ( 𝑁 ‘ 𝑉 ) )
117 113 116 elind ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) )
118 6 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
119 117 118 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ { 0 } )
120 elsni ⊢ ( 𝐶 ∈ { 0 } → 𝐶 = 0 )
121 119 120 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 = 0 )
122 2 0nellinds ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LIndS ‘ 𝑊 ) ) → ¬ 0 ∈ 𝑈 )
123 3 4 122 syl2anc ⊢ ( 𝜑 → ¬ 0 ∈ 𝑈 )
124 nelne2 ⊢ ( ( 𝐶 ∈ 𝑈 ∧ ¬ 0 ∈ 𝑈 ) → 𝐶 ≠ 0 )
125 9 123 124 syl2anc ⊢ ( 𝜑 → 𝐶 ≠ 0 )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ≠ 0 )
127 126 neneqd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑉 ) → ¬ 𝐶 = 0 )
128 121 127 pm2.65da ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝑉 )
129 disjsn ⊢ ( ( 𝑉 ∩ { 𝐶 } ) = ∅ ↔ ¬ 𝐶 ∈ 𝑉 )
130 128 129 sylibr ⊢ ( 𝜑 → ( 𝑉 ∩ { 𝐶 } ) = ∅ )
131 undif4 ⊢ ( ( 𝑉 ∩ { 𝐶 } ) = ∅ → ( 𝑉 ∪ ( 𝑈 ∖ { 𝐶 } ) ) = ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝐶 } ) )
132 130 131 syl ⊢ ( 𝜑 → ( 𝑉 ∪ ( 𝑈 ∖ { 𝐶 } ) ) = ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝐶 } ) )
133 uncom ⊢ ( ( 𝑈 ∖ { 𝐶 } ) ∪ 𝑉 ) = ( 𝑉 ∪ ( 𝑈 ∖ { 𝐶 } ) )
134 uncom ⊢ ( 𝑈 ∪ 𝑉 ) = ( 𝑉 ∪ 𝑈 )
135 134 difeq1i ⊢ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) = ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝐶 } )
136 132 133 135 3eqtr4g ⊢ ( 𝜑 → ( ( 𝑈 ∖ { 𝐶 } ) ∪ 𝑉 ) = ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) )
137 136 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝑈 ∖ { 𝐶 } ) ∪ 𝑉 ) ) = ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) ) )
138 112 137 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) = ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝐶 } ) ) )
139 11 138 eleqtrrd ⊢ ( 𝜑 → ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) )
140 41 110 lsmelval ⊢ ( ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) ↔ ∃ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∃ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ) )
141 140 biimpa ⊢ ( ( ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) ∈ ( ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ 𝑉 ) ) ) → ∃ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∃ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) )
142 105 109 139 141 syl21anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑁 ‘ ( 𝑈 ∖ { 𝐶 } ) ) ∃ 𝑦 ∈ ( 𝑁 ‘ 𝑉 ) ( 𝐾 ( ·𝑠 ‘ 𝑊 ) 𝐶 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) )
143 100 142 r19.29vva ⊢ ( 𝜑 → ⊥ )