linds2eq

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

	Ref	Expression
Hypotheses	linds2eq.1	$⊢ F = {Base}_{Scalar (W)}$
	linds2eq.2	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	linds2eq.3	$⊢ \underset{˙}{+} = +_{W}$
	linds2eq.4	$⊢ \underset{˙}{0} = 0_{Scalar (W)}$
	linds2eq.5	$⊢ φ \to W \in LVec$
	linds2eq.6	$⊢ φ \to B \in LIndS (W)$
	linds2eq.7	$⊢ φ \to X \in B$
	linds2eq.8	$⊢ φ \to Y \in B$
	linds2eq.9	$⊢ φ \to K \in F$
	linds2eq.10	$⊢ φ \to L \in F$
	linds2eq.11	$⊢ φ \to K \neq \underset{˙}{0}$
	linds2eq.12	$⊢ φ \to K \underset{˙}{\cdot} X = L \underset{˙}{\cdot} Y$
Assertion	linds2eq	$⊢ φ \to (X = Y \land K = L)$

Proof

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

Metamath Proof Explorer

Theorem linds2eq

Proof