lss1d - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lss1d		GIF version

Theorem lss1d 13879

Description: One-dimensional subspace (or zero-dimensional if 𝑋 is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)

**Hypotheses**
Ref	Expression
lss1d.v	⊢ 𝑉 = (Base‘𝑊)
lss1d.f	⊢ 𝐹 = (Scalar‘𝑊)
lss1d.t	⊢ · = ( ·_𝑠 ‘𝑊)
lss1d.k	⊢ 𝐾 = (Base‘𝐹)
lss1d.s	⊢ 𝑆 = (LSubSp‘𝑊)

**Assertion**
Ref	Expression
lss1d	⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆)

Distinct variable groups: 𝑣,𝑘,𝐾 · ,𝑘,𝑣 𝑘,𝑉,𝑣 𝑘,𝐹 𝑘,𝑊,𝑣 𝑘,𝑋,𝑣 Allowed substitution hints: 𝑆(𝑣,𝑘) 𝐹(𝑣)

Proof of Theorem lss1d Dummy variables 𝑎 𝑏 𝑗 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lss1d.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	a1i 9	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 = (Scalar‘𝑊))
3		lss1d.k	. . 3 ⊢ 𝐾 = (Base‘𝐹)
4	3	a1i 9	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐾 = (Base‘𝐹))
5		lss1d.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
6	5	a1i 9	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑉 = (Base‘𝑊))
7		eqidd 2194	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (+_g‘𝑊) = (+_g‘𝑊))
8		lss1d.t	. . 3 ⊢ · = ( ·_𝑠 ‘𝑊)
9	8	a1i 9	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → · = ( ·_𝑠 ‘𝑊))
10		lss1d.s	. . 3 ⊢ 𝑆 = (LSubSp‘𝑊)
11	10	a1i 9	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑆 = (LSubSp‘𝑊))
12	5, 1, 8, 3	lmodvscl 13801	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉)
13	12	3expa 1205	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾) ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉)
14	13	an32s 568	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑘 · 𝑋) ∈ 𝑉)
15		eleq1a 2265	. . . . 5 ⊢ ((𝑘 · 𝑋) ∈ 𝑉 → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉))
16	14, 15	syl 14	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉))
17	16	rexlimdva 2611	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉))
18	17	abssdv 3253	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ⊆ 𝑉)
19		eqid 2193	. . . . . 6 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
20	1, 3, 19	lmod0cl 13810	. . . . 5 ⊢ (𝑊 ∈ LMod → (0_g‘𝐹) ∈ 𝐾)
21		elex2 2776	. . . . 5 ⊢ ((0_g‘𝐹) ∈ 𝐾 → ∃𝑘 𝑘 ∈ 𝐾)
22	20, 21	syl 14	. . . 4 ⊢ (𝑊 ∈ LMod → ∃𝑘 𝑘 ∈ 𝐾)
23	22	adantr 276	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ∃𝑘 𝑘 ∈ 𝐾)
24		nfv 1539	. . . 4 ⊢ Ⅎ𝑘(𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)
25		nfre1 2537	. . . . . 6 ⊢ Ⅎ𝑘∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)
26	25	nfsab 2185	. . . . 5 ⊢ Ⅎ𝑘 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}
27	26	nfex 1648	. . . 4 ⊢ Ⅎ𝑘∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}
28		vex 2763	. . . . . . . 8 ⊢ 𝑘 ∈ V
29		vscaslid 12780	. . . . . . . . . . 11 ⊢ ( ·_𝑠 = Slot ( ·_𝑠 ‘ndx) ∧ ( ·_𝑠 ‘ndx) ∈ ℕ)
30	29	slotex 12645	. . . . . . . . . 10 ⊢ (𝑊 ∈ LMod → ( ·_𝑠 ‘𝑊) ∈ V)
31	8, 30	eqeltrid 2280	. . . . . . . . 9 ⊢ (𝑊 ∈ LMod → · ∈ V)
32	31	adantr 276	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → · ∈ V)
33		simpr 110	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
34		ovexg 5952	. . . . . . . 8 ⊢ ((𝑘 ∈ V ∧ · ∈ V ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ V)
35	28, 32, 33, 34	mp3an2i 1353	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ V)
36		elabrexg 5801	. . . . . . 7 ⊢ ((𝑘 ∈ 𝐾 ∧ (𝑘 · 𝑋) ∈ V) → (𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
37	35, 36	sylan2 286	. . . . . 6 ⊢ ((𝑘 ∈ 𝐾 ∧ (𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)) → (𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
38		elex2 2776	. . . . . 6 ⊢ ((𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → ∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
39	37, 38	syl 14	. . . . 5 ⊢ ((𝑘 ∈ 𝐾 ∧ (𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉)) → ∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
40	39	expcom 116	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑘 ∈ 𝐾 → ∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}))
41	24, 27, 40	exlimd 1608	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑘 𝑘 ∈ 𝐾 → ∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}))
42	23, 41	mpd 13	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ∃𝑗 𝑗 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
43		vex 2763	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
44		eqeq1 2200	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑎 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑘 · 𝑋)))
45	44	rexbidv 2495	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑎 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋)))
46	43, 45	elab 2904	. . . . . . . . . 10 ⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋))
47		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑦 → (𝑘 · 𝑋) = (𝑦 · 𝑋))
48	47	eqeq2d 2205	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑦 → (𝑎 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑦 · 𝑋)))
49	48	cbvrexvw 2731	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋) ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋))
50	46, 49	bitri 184	. . . . . . . . 9 ⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋))
51		vex 2763	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
52		eqeq1 2200	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑏 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑘 · 𝑋)))
53	52	rexbidv 2495	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑏 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋)))
54	51, 53	elab 2904	. . . . . . . . . 10 ⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋))
55		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑧 → (𝑘 · 𝑋) = (𝑧 · 𝑋))
56	55	eqeq2d 2205	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑧 → (𝑏 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑧 · 𝑋)))
57	56	cbvrexvw 2731	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋) ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))
58	54, 57	bitri 184	. . . . . . . . 9 ⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))
59	50, 58	anbi12i 460	. . . . . . . 8 ⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)))
60		reeanv 2664	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)))
61	59, 60	bitr4i 187	. . . . . . 7 ⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ ∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)))
62		simpll 527	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑊 ∈ LMod)
63		simprr 531	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑥 ∈ 𝐾)
64		simprll 537	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑦 ∈ 𝐾)
65		eqid 2193	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝐹) = (._r‘𝐹)
66	1, 3, 65	lmodmcl 13796	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑥(._r‘𝐹)𝑦) ∈ 𝐾)
67	62, 63, 64, 66	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (𝑥(._r‘𝐹)𝑦) ∈ 𝐾)
68		simprlr 538	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑧 ∈ 𝐾)
69		eqid 2193	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐹) = (+_g‘𝐹)
70	1, 3, 69	lmodacl 13795	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ (𝑥(._r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → ((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) ∈ 𝐾)
71	62, 67, 68, 70	syl3anc 1249	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) ∈ 𝐾)
72		simplr 528	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑋 ∈ 𝑉)
73		eqid 2193	. . . . . . . . . . . . . . 15 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
74	5, 73, 1, 8, 3, 69	lmodvsdir 13808	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ ((𝑥(._r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) · 𝑋) = (((𝑥(._r‘𝐹)𝑦) · 𝑋)(+_g‘𝑊)(𝑧 · 𝑋)))
75	62, 67, 68, 72, 74	syl13anc 1251	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) · 𝑋) = (((𝑥(._r‘𝐹)𝑦) · 𝑋)(+_g‘𝑊)(𝑧 · 𝑋)))
76	5, 1, 8, 3, 65	lmodvsass 13809	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑥(._r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋)))
77	62, 63, 64, 72, 76	syl13anc 1251	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(._r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋)))
78	77	oveq1d 5933	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(._r‘𝐹)𝑦) · 𝑋)(+_g‘𝑊)(𝑧 · 𝑋)) = ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)))
79	75, 78	eqtr2d 2227	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) · 𝑋))
80		oveq1 5925	. . . . . . . . . . . . 13 ⊢ (𝑘 = ((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) → (𝑘 · 𝑋) = (((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) · 𝑋))
81	80	rspceeqv 2882	. . . . . . . . . . . 12 ⊢ ((((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) ∈ 𝐾 ∧ ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(._r‘𝐹)𝑦)(+_g‘𝐹)𝑧) · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))
82	71, 79, 81	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))
83		oveq2 5926	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑦 · 𝑋) → (𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋)))
84		oveq12 5927	. . . . . . . . . . . . . 14 ⊢ (((𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋)) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)))
85	83, 84	sylan 283	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)))
86	85	eqeq1d 2202	. . . . . . . . . . . 12 ⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)))
87	86	rexbidv 2495	. . . . . . . . . . 11 ⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+_g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)))
88	82, 87	syl5ibrcom 157	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
89	88	expr 375	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑥 ∈ 𝐾 → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋))))
90	89	com23 78	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋))))
91	90	rexlimdvva 2619	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋))))
92	61, 91	biimtrid 152	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋))))
93	92	expcomd 1452	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))))
94	93	com24 87	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ 𝐾 → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))))
95	94	3imp2 1224	. . 3 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋))
96		vex 2763	. . . . . . 7 ⊢ 𝑥 ∈ V
97	43	a1i 9	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝑎 ∈ V)
98		ovexg 5952	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ · ∈ V ∧ 𝑎 ∈ V) → (𝑥 · 𝑎) ∈ V)
99	96, 31, 97, 98	mp3an2i 1353	. . . . . 6 ⊢ (𝑊 ∈ LMod → (𝑥 · 𝑎) ∈ V)
100		plusgslid 12730	. . . . . . 7 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
101	100	slotex 12645	. . . . . 6 ⊢ (𝑊 ∈ LMod → (+_g‘𝑊) ∈ V)
102	51	a1i 9	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝑏 ∈ V)
103		ovexg 5952	. . . . . 6 ⊢ (((𝑥 · 𝑎) ∈ V ∧ (+_g‘𝑊) ∈ V ∧ 𝑏 ∈ V) → ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ V)
104	99, 101, 102, 103	syl3anc 1249	. . . . 5 ⊢ (𝑊 ∈ LMod → ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ V)
105		eqeq1 2200	. . . . . . 7 ⊢ (𝑣 = ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) → (𝑣 = (𝑘 · 𝑋) ↔ ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
106	105	rexbidv 2495	. . . . . 6 ⊢ (𝑣 = ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
107	106	elabg 2906	. . . . 5 ⊢ (((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ V → (((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
108	104, 107	syl 14	. . . 4 ⊢ (𝑊 ∈ LMod → (((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
109	108	ad2antrr 488	. . 3 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → (((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) = (𝑘 · 𝑋)))
110	95, 109	mpbird 167	. 2 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ((𝑥 · 𝑎)(+_g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})
111		simpl 109	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑊 ∈ LMod)
112	2, 4, 6, 7, 9, 11, 18, 42, 110, 111	islssmd 13855	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∃wex 1503 ∈ wcel 2164 {cab 2179 ∃wrex 2473 Vcvv 2760 ‘cfv 5254 (class class class)co 5918 Basecbs 12618 +_gcplusg 12695 ._rcmulr 12696 Scalarcsca 12698 ·_𝑠 cvsca 12699 0_gc0g 12867 LModclmod 13783 LSubSpclss 13848

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-i2m1 7977 ax-0lt1 7978 ax-0id 7980 ax-rnegex 7981 ax-pre-ltirr 7984 ax-pre-ltadd 7988

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-br 4030 df-opab 4091 df-mpt 4092 df-id 4324 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-iota 5215 df-fun 5256 df-fn 5257 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-pnf 8056 df-mnf 8057 df-ltxr 8059 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-5 9044 df-6 9045 df-ndx 12621 df-slot 12622 df-base 12624 df-sets 12625 df-plusg 12708 df-mulr 12709 df-sca 12711 df-vsca 12712 df-0g 12869 df-mgm 12939 df-sgrp 12985 df-mnd 12998 df-grp 13075 df-mgp 13417 df-ring 13494 df-lmod 13785 df-lssm 13849

This theorem is referenced by: lspsn 13912

W3C validator