linds2eq

Description: Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023)

	Ref	Expression
Hypotheses	linds2eq.1	⊢ 𝐹 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
	linds2eq.2	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	linds2eq.3	⊢ + = ( +_g ‘ 𝑊 )
	linds2eq.4	⊢ 0 = ( 0_g ‘ ( Scalar ‘ 𝑊 ) )
	linds2eq.5	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	linds2eq.6	⊢ ( 𝜑 → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
	linds2eq.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	linds2eq.8	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	linds2eq.9	⊢ ( 𝜑 → 𝐾 ∈ 𝐹 )
	linds2eq.10	⊢ ( 𝜑 → 𝐿 ∈ 𝐹 )
	linds2eq.11	⊢ ( 𝜑 → 𝐾 ≠ 0 )
	linds2eq.12	⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) )
Assertion	linds2eq	⊢ ( 𝜑 → ( 𝑋 = 𝑌 ∧ 𝐾 = 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		linds2eq.1	⊢ 𝐹 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
2		linds2eq.2	⊢ · = ( ·_𝑠 ‘ 𝑊 )
3		linds2eq.3	⊢ + = ( +_g ‘ 𝑊 )
4		linds2eq.4	⊢ 0 = ( 0_g ‘ ( Scalar ‘ 𝑊 ) )
5		linds2eq.5	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		linds2eq.6	⊢ ( 𝜑 → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
7		linds2eq.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		linds2eq.8	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		linds2eq.9	⊢ ( 𝜑 → 𝐾 ∈ 𝐹 )
10		linds2eq.10	⊢ ( 𝜑 → 𝐿 ∈ 𝐹 )
11		linds2eq.11	⊢ ( 𝜑 → 𝐾 ≠ 0 )
12		linds2eq.12	⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
14	12	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) )
15	13	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐿 · 𝑋 ) = ( 𝐿 · 𝑌 ) )
16	14 15	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑋 ) )
17		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
18		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
19		eqid	⊢ ( 0_g ‘ 𝑊 ) = ( 0_g ‘ 𝑊 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑊 ∈ LVec )
21	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐾 ∈ 𝐹 )
22	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐿 ∈ 𝐹 )
23	17	linds1	⊢ ( 𝐵 ∈ ( LIndS ‘ 𝑊 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
24	6 23	syl	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
25	24 7	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
27	19	0nellinds	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ ( LIndS ‘ 𝑊 ) ) → ¬ ( 0_g ‘ 𝑊 ) ∈ 𝐵 )
28	5 6 27	syl2anc	⊢ ( 𝜑 → ¬ ( 0_g ‘ 𝑊 ) ∈ 𝐵 )
29		nelne2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 0_g ‘ 𝑊 ) ∈ 𝐵 ) → 𝑋 ≠ ( 0_g ‘ 𝑊 ) )
30	7 28 29	syl2anc	⊢ ( 𝜑 → 𝑋 ≠ ( 0_g ‘ 𝑊 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ≠ ( 0_g ‘ 𝑊 ) )
32	17 2 18 1 19 20 21 22 26 31	lvecvscan2	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑋 ) ↔ 𝐾 = 𝐿 ) )
33	16 32	mpbid	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐾 = 𝐿 )
34	13 33	jca	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 = 𝑌 ∧ 𝐾 = 𝐿 ) )
35	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐵 )
36	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐾 ∈ 𝐹 )
37		opex	⊢ ⟨ 𝑋 , 𝐾 ⟩ ∈ V
38	37	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ⟨ 𝑋 , 𝐾 ⟩ ∈ V )
39		opex	⊢ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∈ V
40	39	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∈ V )
41		animorrl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ) )
42		opthneg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) → ( ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ↔ ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ) ) )
43	42	biimpar	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) ∧ ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ) ) → ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ )
44	35 36 41 43	syl21anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ )
45		animorrl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ 0 ) )
46		opthneg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) → ( ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ ↔ ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ 0 ) ) )
47	46	biimpar	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) ∧ ( 𝑋 ≠ 𝑌 ∨ 𝐾 ≠ 0 ) ) → ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ )
48	35 36 45 47	syl21anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ )
49	44 48	jca	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∧ ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ ) )
50	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐵 )
51		fvexd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ V )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
53		fprg	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝐹 ∧ ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ V ) ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝐾 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) } )
54	35 50 36 51 52 53	syl221anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝐾 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) } )
55		prfi	⊢ { 𝑋 , 𝑌 } ∈ Fin
56	55	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ∈ Fin )
57	4	fvexi	⊢ 0 ∈ V
58	57	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 0 ∈ V )
59	54 56 58	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } finSupp 0 )
60		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
61	5 60	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
62		lmodcmn	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )
63	61 62	syl	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑊 ∈ CMnd )
65	61	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑊 ∈ LMod )
66	18	lmodring	⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
67		ringgrp	⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ Grp )
68	61 66 67	3syl	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ Grp )
69		eqid	⊢ ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) = ( inv_g ‘ ( Scalar ‘ 𝑊 ) )
70	1 69	grpinvcl	⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ 𝐿 ∈ 𝐹 ) → ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ 𝐹 )
71	68 10 70	syl2anc	⊢ ( 𝜑 → ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ 𝐹 )
72	9 71	prssd	⊢ ( 𝜑 → { 𝐾 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) } ⊆ 𝐹 )
73	72	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝐾 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) } ⊆ 𝐹 )
74	54 73	fssd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ 𝐹 )
75		eqidd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 = 𝑋 )
76	75	orcd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 = 𝑋 ∨ 𝑋 = 𝑌 ) )
77		elprg	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ { 𝑋 , 𝑌 } ↔ ( 𝑋 = 𝑋 ∨ 𝑋 = 𝑌 ) ) )
78	77	biimpar	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 = 𝑋 ∨ 𝑋 = 𝑌 ) ) → 𝑋 ∈ { 𝑋 , 𝑌 } )
79	35 76 78	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ { 𝑋 , 𝑌 } )
80	74 79	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) ∈ 𝐹 )
81	25	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
82	17 18 2 1	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) ∈ 𝐹 ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
83	65 80 81 82	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
84		eqidd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 = 𝑌 )
85	84	olcd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 = 𝑋 ∨ 𝑌 = 𝑌 ) )
86		elprg	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑌 ∈ { 𝑋 , 𝑌 } ↔ ( 𝑌 = 𝑋 ∨ 𝑌 = 𝑌 ) ) )
87	86	biimpar	⊢ ( ( 𝑌 ∈ 𝐵 ∧ ( 𝑌 = 𝑋 ∨ 𝑌 = 𝑌 ) ) → 𝑌 ∈ { 𝑋 , 𝑌 } )
88	50 85 87	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ { 𝑋 , 𝑌 } )
89	74 88	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) ∈ 𝐹 )
90	24 8	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑊 ) )
91	90	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
92	17 18 2 1	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) ∈ 𝐹 ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
93	65 89 91 92	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
94		fveq2	⊢ ( 𝑏 = 𝑋 → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) = ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) )
95		id	⊢ ( 𝑏 = 𝑋 → 𝑏 = 𝑋 )
96	94 95	oveq12d	⊢ ( 𝑏 = 𝑋 → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) = ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) )
97		fveq2	⊢ ( 𝑏 = 𝑌 → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) = ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) )
98		id	⊢ ( 𝑏 = 𝑌 → 𝑏 = 𝑌 )
99	97 98	oveq12d	⊢ ( 𝑏 = 𝑌 → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) = ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) )
100	17 3 96 99	gsumpr	⊢ ( ( 𝑊 ∈ CMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ ( ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) + ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ) )
101	64 35 50 52 83 93 100	syl132anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) + ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ) )
102		fvpr1g	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) = 𝐾 )
103	35 36 52 102	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) = 𝐾 )
104	103	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) = ( 𝐾 · 𝑋 ) )
105	71	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ 𝐹 )
106		fvpr2g	⊢ ( ( 𝑌 ∈ 𝐵 ∧ ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ∈ 𝐹 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) = ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) )
107	50 105 52 106	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) = ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) )
108	107	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) = ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) )
109	104 108	oveq12d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑋 ) · 𝑋 ) + ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑌 ) · 𝑌 ) ) = ( ( 𝐾 · 𝑋 ) + ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) ) )
110	17 18 2 1	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐾 · 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
111	61 9 25 110	syl3anc	⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
112	12 111	eqeltrrd	⊢ ( 𝜑 → ( 𝐿 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
113		eqid	⊢ ( inv_g ‘ 𝑊 ) = ( inv_g ‘ 𝑊 )
114		eqid	⊢ ( -_g ‘ 𝑊 ) = ( -_g ‘ 𝑊 )
115	17 3 113 114	grpsubval	⊢ ( ( ( 𝐾 · 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐿 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐾 · 𝑋 ) ( -_g ‘ 𝑊 ) ( 𝐿 · 𝑌 ) ) = ( ( 𝐾 · 𝑋 ) + ( ( inv_g ‘ 𝑊 ) ‘ ( 𝐿 · 𝑌 ) ) ) )
116	111 112 115	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 · 𝑋 ) ( -_g ‘ 𝑊 ) ( 𝐿 · 𝑌 ) ) = ( ( 𝐾 · 𝑋 ) + ( ( inv_g ‘ 𝑊 ) ‘ ( 𝐿 · 𝑌 ) ) ) )
117		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
118	61 117	syl	⊢ ( 𝜑 → 𝑊 ∈ Grp )
119	17 19 114	grpsubeq0	⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝐾 · 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐿 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝐾 · 𝑋 ) ( -_g ‘ 𝑊 ) ( 𝐿 · 𝑌 ) ) = ( 0_g ‘ 𝑊 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) ) )
120	118 111 112 119	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐾 · 𝑋 ) ( -_g ‘ 𝑊 ) ( 𝐿 · 𝑌 ) ) = ( 0_g ‘ 𝑊 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) ) )
121	12 120	mpbird	⊢ ( 𝜑 → ( ( 𝐾 · 𝑋 ) ( -_g ‘ 𝑊 ) ( 𝐿 · 𝑌 ) ) = ( 0_g ‘ 𝑊 ) )
122	17 18 2 113 1 69 61 90 10	lmodvsneg	⊢ ( 𝜑 → ( ( inv_g ‘ 𝑊 ) ‘ ( 𝐿 · 𝑌 ) ) = ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) )
123	122	oveq2d	⊢ ( 𝜑 → ( ( 𝐾 · 𝑋 ) + ( ( inv_g ‘ 𝑊 ) ‘ ( 𝐿 · 𝑌 ) ) ) = ( ( 𝐾 · 𝑋 ) + ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) ) )
124	116 121 123	3eqtr3rd	⊢ ( 𝜑 → ( ( 𝐾 · 𝑋 ) + ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) ) = ( 0_g ‘ 𝑊 ) )
125	124	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐾 · 𝑋 ) + ( ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) · 𝑌 ) ) = ( 0_g ‘ 𝑊 ) )
126	101 109 125	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) )
127		breq1	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( 𝑎 finSupp 0 ↔ { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } finSupp 0 ) )
128		fveq1	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( 𝑎 ‘ 𝑏 ) = ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) )
129	128	oveq1d	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) = ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) )
130	129	mpteq2dv	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) = ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) )
131	130	oveq2d	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) )
132	131	eqeq1d	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ↔ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) )
133	127 132	anbi12d	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) ↔ ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) ) )
134		eqeq1	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ↔ { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = ( { 𝑋 , 𝑌 } × { 0 } ) ) )
135	133 134	imbi12d	⊢ ( 𝑎 = { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } → ( ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ) ↔ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = ( { 𝑋 , 𝑌 } × { 0 } ) ) ) )
136	7 8	prssd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝐵 )
137	136 24	sstrd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ ( Base ‘ 𝑊 ) )
138		lindsss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ ( LIndS ‘ 𝑊 ) ∧ { 𝑋 , 𝑌 } ⊆ 𝐵 ) → { 𝑋 , 𝑌 } ∈ ( LIndS ‘ 𝑊 ) )
139	61 6 136 138	syl3anc	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ∈ ( LIndS ‘ 𝑊 ) )
140	17 1 18 2 19 4	islinds5	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ ( Base ‘ 𝑊 ) ) → ( { 𝑋 , 𝑌 } ∈ ( LIndS ‘ 𝑊 ) ↔ ∀ 𝑎 ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ) ) )
141	140	biimpa	⊢ ( ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ ( Base ‘ 𝑊 ) ) ∧ { 𝑋 , 𝑌 } ∈ ( LIndS ‘ 𝑊 ) ) → ∀ 𝑎 ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ) )
142	61 137 139 141	syl21anc	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ) )
143	142	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ∀ 𝑎 ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( 𝑎 ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → 𝑎 = ( { 𝑋 , 𝑌 } × { 0 } ) ) )
144	1	fvexi	⊢ 𝐹 ∈ V
145	144	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐹 ∈ V )
146	139	elexd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ∈ V )
147	146	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ∈ V )
148	145 147	elmapd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) ↔ { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ 𝐹 ) )
149	74 148	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ∈ ( 𝐹 ↑_m { 𝑋 , 𝑌 } ) )
150	135 143 149	rspcdva	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } finSupp 0 ∧ ( 𝑊 Σ_g ( 𝑏 ∈ { 𝑋 , 𝑌 } ↦ ( ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } ‘ 𝑏 ) · 𝑏 ) ) ) = ( 0_g ‘ 𝑊 ) ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = ( { 𝑋 , 𝑌 } × { 0 } ) ) )
151	59 126 150	mp2and	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = ( { 𝑋 , 𝑌 } × { 0 } ) )
152		xpprsng	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 0 ∈ V ) → ( { 𝑋 , 𝑌 } × { 0 } ) = { ⟨ 𝑋 , 0 ⟩ , ⟨ 𝑌 , 0 ⟩ } )
153	35 50 58 152	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( { 𝑋 , 𝑌 } × { 0 } ) = { ⟨ 𝑋 , 0 ⟩ , ⟨ 𝑌 , 0 ⟩ } )
154	151 153	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ , ⟨ 𝑌 , 0 ⟩ } )
155		opthprneg	⊢ ( ( ( ⟨ 𝑋 , 𝐾 ⟩ ∈ V ∧ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∈ V ) ∧ ( ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∧ ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ ) ) → ( { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ , ⟨ 𝑌 , 0 ⟩ } ↔ ( ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ ∧ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ = ⟨ 𝑌 , 0 ⟩ ) ) )
156	155	biimpa	⊢ ( ( ( ( ⟨ 𝑋 , 𝐾 ⟩ ∈ V ∧ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∈ V ) ∧ ( ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ ∧ ⟨ 𝑋 , 𝐾 ⟩ ≠ ⟨ 𝑌 , 0 ⟩ ) ) ∧ { ⟨ 𝑋 , 𝐾 ⟩ , ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ , ⟨ 𝑌 , 0 ⟩ } ) → ( ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ ∧ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ = ⟨ 𝑌 , 0 ⟩ ) )
157	38 40 49 154 156	syl1111anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ ∧ ⟨ 𝑌 , ( ( inv_g ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝐿 ) ⟩ = ⟨ 𝑌 , 0 ⟩ ) )
158	157	simpld	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ )
159		opthg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) → ( ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ ↔ ( 𝑋 = 𝑋 ∧ 𝐾 = 0 ) ) )
160	159	simplbda	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝐾 ∈ 𝐹 ) ∧ ⟨ 𝑋 , 𝐾 ⟩ = ⟨ 𝑋 , 0 ⟩ ) → 𝐾 = 0 )
161	35 36 158 160	syl21anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐾 = 0 )
162	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐾 ≠ 0 )
163	161 162	pm2.21ddne	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 = 𝑌 ∧ 𝐾 = 𝐿 ) )
164	34 163	pm2.61dane	⊢ ( 𝜑 → ( 𝑋 = 𝑌 ∧ 𝐾 = 𝐿 ) )

Metamath Proof Explorer

Theorem linds2eq

Proof