lspexch

Description: Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 versus lspexchn2 ); look for lspexch and prcom in same proof. TODO: would a hypothesis of -. X e. ( N{ Z } ) instead of ( N{ X } ) =/= ( N{ Z } ) be better overall? This would be shorter and also satisfy the X =/= .0. condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the =/= pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015)

	Ref	Expression
Hypotheses	lspexch.v	$⊢ V = {Base}_{W}$
	lspexch.o	$⊢ \underset{˙}{0} = 0_{W}$
	lspexch.n	$⊢ N = LSpan (W)$
	lspexch.w	$⊢ φ \to W \in LVec$
	lspexch.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lspexch.y	$⊢ φ \to Y \in V$
	lspexch.z	$⊢ φ \to Z \in V$
	lspexch.q	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
	lspexch.e	$⊢ φ \to X \in N (\{Y, Z\})$
Assertion	lspexch	$⊢ φ \to Y \in N (\{X, Z\})$

Proof

Step	Hyp	Ref	Expression
1		lspexch.v	$⊢ V = {Base}_{W}$
2		lspexch.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspexch.n	$⊢ N = LSpan (W)$
4		lspexch.w	$⊢ φ \to W \in LVec$
5		lspexch.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
6		lspexch.y	$⊢ φ \to Y \in V$
7		lspexch.z	$⊢ φ \to Z \in V$
8		lspexch.q	$⊢ φ \to N (\{X\}) \neq N (\{Z\})$
9		lspexch.e	$⊢ φ \to X \in N (\{Y, Z\})$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
13		eqid	$⊢ \cdot_{W} = \cdot_{W}$
14		lveclmod	$⊢ W \in LVec \to W \in LMod$
15	4 14	syl	$⊢ φ \to W \in LMod$
16	1 10 11 12 13 3 15 6 7	lspprel	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow \exists j \in {Base}_{Scalar (W)} \exists k \in {Base}_{Scalar (W)} X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z))$
17	9 16	mpbid	$⊢ φ \to \exists j \in {Base}_{Scalar (W)} \exists k \in {Base}_{Scalar (W)} X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)$
18		eqid	$⊢ -_{W} = -_{W}$
19		eqid	$⊢ {inv}_{g} (Scalar (W)) = {inv}_{g} (Scalar (W))$
20	4	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to W \in LVec$
21	20 14	syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to W \in LMod$
22		simp2r	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to k \in {Base}_{Scalar (W)}$
23	5	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X \in (V ∖ \{\underset{˙}{0}\})$
24	23	eldifad	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X \in V$
25	7	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Z \in V$
26	1 10 18 13 11 12 19 21 22 24 25	lmodsubvs	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X -_{W} (k \cdot_{W} Z) = X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z)$
27		simp3	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)$
28	27	eqcomd	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = X$
29	15	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to W \in LMod$
30		lmodgrp	$⊢ W \in LMod \to W \in Grp$
31	29 30	syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to W \in Grp$
32	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land Z \in V) \to k \cdot_{W} Z \in V$
33	21 22 25 32	syl3anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to k \cdot_{W} Z \in V$
34		simp2l	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to j \in {Base}_{Scalar (W)}$
35	6	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Y \in V$
36	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land j \in {Base}_{Scalar (W)} \land Y \in V) \to j \cdot_{W} Y \in V$
37	21 34 35 36	syl3anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to j \cdot_{W} Y \in V$
38	1 10 18	grpsubadd	$⊢ (W \in Grp \land (X \in V \land k \cdot_{W} Z \in V \land j \cdot_{W} Y \in V)) \to (X -_{W} (k \cdot_{W} Z) = j \cdot_{W} Y \leftrightarrow (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = X)$
39	31 24 33 37 38	syl13anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (X -_{W} (k \cdot_{W} Z) = j \cdot_{W} Y \leftrightarrow (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = X)$
40	28 39	mpbird	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X -_{W} (k \cdot_{W} Z) = j \cdot_{W} Y$
41	26 40	eqtr3d	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) = j \cdot_{W} Y$
42		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
43		eqid	$⊢ {inv}_{r} (Scalar (W)) = {inv}_{r} (Scalar (W))$
44	8	3ad2ant1	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to N (\{X\}) \neq N (\{Z\})$
45	20	adantr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to W \in LVec$
46	25	adantr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to Z \in V$
47	27	adantr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)$
48		oveq1	$⊢ j = 0_{Scalar (W)} \to j \cdot_{W} Y = 0_{Scalar (W)} \cdot_{W} Y$
49	48	oveq1d	$⊢ j = 0_{Scalar (W)} \to (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = (0_{Scalar (W)} \cdot_{W} Y) +_{W} (k \cdot_{W} Z)$
50	1 11 13 42 2	lmod0vs	$⊢ (W \in LMod \land Y \in V) \to 0_{Scalar (W)} \cdot_{W} Y = \underset{˙}{0}$
51	21 35 50	syl2anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to 0_{Scalar (W)} \cdot_{W} Y = \underset{˙}{0}$
52	51	oveq1d	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (0_{Scalar (W)} \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = \underset{˙}{0} +_{W} (k \cdot_{W} Z)$
53	1 10 2	lmod0vlid	$⊢ (W \in LMod \land k \cdot_{W} Z \in V) \to \underset{˙}{0} +_{W} (k \cdot_{W} Z) = k \cdot_{W} Z$
54	21 33 53	syl2anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to \underset{˙}{0} +_{W} (k \cdot_{W} Z) = k \cdot_{W} Z$
55	52 54	eqtrd	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (0_{Scalar (W)} \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = k \cdot_{W} Z$
56	49 55	sylan9eqr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) = k \cdot_{W} Z$
57	47 56	eqtrd	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to X = k \cdot_{W} Z$
58	1 13 11 12 3 21 22 25	ellspsni	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to k \cdot_{W} Z \in N (\{Z\})$
59	58	adantr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to k \cdot_{W} Z \in N (\{Z\})$
60	57 59	eqeltrd	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to X \in N (\{Z\})$
61		eldifsni	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
62	23 61	syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X \neq \underset{˙}{0}$
63	62	adantr	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to X \neq \underset{˙}{0}$
64	1 2 3 45 46 60 63	lspsneleq	$⊢ ((φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \land j = 0_{Scalar (W)}) \to N (\{X\}) = N (\{Z\})$
65	64	ex	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (j = 0_{Scalar (W)} \to N (\{X\}) = N (\{Z\}))$
66	65	necon3d	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (N (\{X\}) \neq N (\{Z\}) \to j \neq 0_{Scalar (W)})$
67	44 66	mpd	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to j \neq 0_{Scalar (W)}$
68		eldifsn	$⊢ j \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (j \in {Base}_{Scalar (W)} \land j \neq 0_{Scalar (W)})$
69	34 67 68	sylanbrc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to j \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})$
70	11	lmodfgrp	$⊢ W \in LMod \to Scalar (W) \in Grp$
71	29 70	syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Scalar (W) \in Grp$
72	12 19	grpinvcl	$⊢ (Scalar (W) \in Grp \land k \in {Base}_{Scalar (W)}) \to {inv}_{g} (Scalar (W)) (k) \in {Base}_{Scalar (W)}$
73	71 22 72	syl2anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to {inv}_{g} (Scalar (W)) (k) \in {Base}_{Scalar (W)}$
74	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land {inv}_{g} (Scalar (W)) (k) \in {Base}_{Scalar (W)} \land Z \in V) \to {inv}_{g} (Scalar (W)) (k) \cdot_{W} Z \in V$
75	21 73 25 74	syl3anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to {inv}_{g} (Scalar (W)) (k) \cdot_{W} Z \in V$
76	1 10	lmodvacl	$⊢ (W \in LMod \land X \in V \land {inv}_{g} (Scalar (W)) (k) \cdot_{W} Z \in V) \to X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) \in V$
77	21 24 75 76	syl3anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) \in V$
78	1 13 11 12 42 43 20 69 77 35	lvecinv	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) = j \cdot_{W} Y \leftrightarrow Y = {inv}_{r} (Scalar (W)) (j) \cdot_{W} (X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z)))$
79	41 78	mpbid	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Y = {inv}_{r} (Scalar (W)) (j) \cdot_{W} (X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z))$
80		eqid	$⊢ LSubSp (W) = LSubSp (W)$
81	1 80 3 21 24 25	lspprcl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to N (\{X, Z\}) \in LSubSp (W)$
82	11	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
83	20 82	syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Scalar (W) \in DivRing$
84	12 42 43	drnginvrcl	$⊢ (Scalar (W) \in DivRing \land j \in {Base}_{Scalar (W)} \land j \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (j) \in {Base}_{Scalar (W)}$
85	83 34 67 84	syl3anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (j) \in {Base}_{Scalar (W)}$
86		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
87	1 11 13 86	lmodvs1	$⊢ (W \in LMod \land X \in V) \to 1_{Scalar (W)} \cdot_{W} X = X$
88	21 24 87	syl2anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to 1_{Scalar (W)} \cdot_{W} X = X$
89	88	oveq1d	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (1_{Scalar (W)} \cdot_{W} X) +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) = X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z)$
90	11	lmodring	$⊢ W \in LMod \to Scalar (W) \in Ring$
91	12 86	ringidcl	$⊢ Scalar (W) \in Ring \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
92	21 90 91	3syl	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
93	1 10 13 11 12 3 21 92 73 24 25	lsppreli	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to (1_{Scalar (W)} \cdot_{W} X) +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) \in N (\{X, Z\})$
94	89 93	eqeltrrd	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) \in N (\{X, Z\})$
95	11 13 12 80	lssvscl	$⊢ ((W \in LMod \land N (\{X, Z\}) \in LSubSp (W)) \land ({inv}_{r} (Scalar (W)) (j) \in {Base}_{Scalar (W)} \land X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z) \in N (\{X, Z\}))) \to {inv}_{r} (Scalar (W)) (j) \cdot_{W} (X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z)) \in N (\{X, Z\})$
96	21 81 85 94 95	syl22anc	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (j) \cdot_{W} (X +_{W} ({inv}_{g} (Scalar (W)) (k) \cdot_{W} Z)) \in N (\{X, Z\})$
97	79 96	eqeltrd	$⊢ (φ \land (j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \land X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z)) \to Y \in N (\{X, Z\})$
98	97	3exp	$⊢ φ \to ((j \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)}) \to (X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) \to Y \in N (\{X, Z\})))$
99	98	rexlimdvv	$⊢ φ \to (\exists j \in {Base}_{Scalar (W)} \exists k \in {Base}_{Scalar (W)} X = (j \cdot_{W} Y) +_{W} (k \cdot_{W} Z) \to Y \in N (\{X, Z\}))$
100	17 99	mpd	$⊢ φ \to Y \in N (\{X, Z\})$

Metamath Proof Explorer

Theorem lspexch

Proof