f1lindf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1lindf		Structured version Visualization version GIF version

Theorem f1lindf 20161

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)

**Assertion**
Ref	Expression
f1lindf	⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺) LIndF 𝑊)

Proof of Theorem f1lindf Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑊)
2	1	lindff 20154	. . . . . 6 ⊢ ((𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod) → 𝐹:dom 𝐹⟶(Base‘𝑊))
3	2	ancoms 469	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹⟶(Base‘𝑊))
4	3	3adant3 1081	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐹:dom 𝐹⟶(Base‘𝑊))
5		f1f 6101	. . . . 5 ⊢ (𝐺:𝐾–1-1→dom 𝐹 → 𝐺:𝐾⟶dom 𝐹)
6	5	3ad2ant3 1084	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐺:𝐾⟶dom 𝐹)
7		fco 6058	. . . 4 ⊢ ((𝐹:dom 𝐹⟶(Base‘𝑊) ∧ 𝐺:𝐾⟶dom 𝐹) → (𝐹 ∘ 𝐺):𝐾⟶(Base‘𝑊))
8	4, 6, 7	syl2anc 693	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺):𝐾⟶(Base‘𝑊))
9		ffdm 6062	. . . 4 ⊢ ((𝐹 ∘ 𝐺):𝐾⟶(Base‘𝑊) → ((𝐹 ∘ 𝐺):dom (𝐹 ∘ 𝐺)⟶(Base‘𝑊) ∧ dom (𝐹 ∘ 𝐺) ⊆ 𝐾))
10	9	simpld 475	. . 3 ⊢ ((𝐹 ∘ 𝐺):𝐾⟶(Base‘𝑊) → (𝐹 ∘ 𝐺):dom (𝐹 ∘ 𝐺)⟶(Base‘𝑊))
11	8, 10	syl 17	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺):dom (𝐹 ∘ 𝐺)⟶(Base‘𝑊))
12		simpl2 1065	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝐹 LIndF 𝑊)
13	6	adantr 481	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → 𝐺:𝐾⟶dom 𝐹)
14		fdm 6051	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝐺):𝐾⟶(Base‘𝑊) → dom (𝐹 ∘ 𝐺) = 𝐾)
15	8, 14	syl 17	. . . . . . . . 9 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → dom (𝐹 ∘ 𝐺) = 𝐾)
16	15	eleq2d 2687	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝑥 ∈ dom (𝐹 ∘ 𝐺) ↔ 𝑥 ∈ 𝐾))
17	16	biimpa 501	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → 𝑥 ∈ 𝐾)
18	13, 17	ffvelrnd 6360	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → (𝐺‘𝑥) ∈ dom 𝐹)
19	18	adantrr 753	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝐺‘𝑥) ∈ dom 𝐹)
20		eldifi 3732	. . . . . 6 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
21	20	ad2antll 765	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
22		eldifsni 4320	. . . . . 6 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → 𝑘 ≠ (0_g‘(Scalar‘𝑊)))
23	22	ad2antll 765	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑘 ≠ (0_g‘(Scalar‘𝑊)))
24		eqid 2622	. . . . . 6 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
25		eqid 2622	. . . . . 6 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
26		eqid 2622	. . . . . 6 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
27		eqid 2622	. . . . . 6 ⊢ (0_g‘(Scalar‘𝑊)) = (0_g‘(Scalar‘𝑊))
28		eqid 2622	. . . . . 6 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
29	24, 25, 26, 27, 28	lindfind 20155	. . . . 5 ⊢ (((𝐹 LIndF 𝑊 ∧ (𝐺‘𝑥) ∈ dom 𝐹) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) → ¬ (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))))
30	12, 19, 21, 23, 29	syl22anc 1327	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))))
31		f1fn 6102	. . . . . . . . . . 11 ⊢ (𝐺:𝐾–1-1→dom 𝐹 → 𝐺 Fn 𝐾)
32	31	3ad2ant3 1084	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐺 Fn 𝐾)
33	32	adantr 481	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → 𝐺 Fn 𝐾)
34		fvco2 6273	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐾 ∧ 𝑥 ∈ 𝐾) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥)))
35	33, 17, 34	syl2anc 693	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥)))
36	35	oveq2d 6666	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → (𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) = (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))))
37	36	eleq1d 2686	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → ((𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ↔ (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})))))
38		simpl1 1064	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → 𝑊 ∈ LMod)
39		imassrn 5477	. . . . . . . . . . 11 ⊢ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})) ⊆ ran 𝐹
40		frn 6053	. . . . . . . . . . . 12 ⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → ran 𝐹 ⊆ (Base‘𝑊))
41	4, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → ran 𝐹 ⊆ (Base‘𝑊))
42	39, 41	syl5ss 3614	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})) ⊆ (Base‘𝑊))
43	42	adantr 481	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})) ⊆ (Base‘𝑊))
44		imaco 5640	. . . . . . . . . 10 ⊢ ((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) = (𝐹 “ (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})))
45	15	difeq1d 3727	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (dom (𝐹 ∘ 𝐺) ∖ {𝑥}) = (𝐾 ∖ {𝑥}))
46	45	imaeq2d 5466	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) = (𝐺 “ (𝐾 ∖ {𝑥})))
47		df-f1 5893	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:𝐾–1-1→dom 𝐹 ↔ (𝐺:𝐾⟶dom 𝐹 ∧ Fun ^◡𝐺))
48	47	simprbi 480	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐾–1-1→dom 𝐹 → Fun ^◡𝐺)
49	48	3ad2ant3 1084	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → Fun ^◡𝐺)
50		imadif 5973	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡𝐺 → (𝐺 “ (𝐾 ∖ {𝑥})) = ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})))
51	49, 50	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐺 “ (𝐾 ∖ {𝑥})) = ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})))
52	46, 51	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) = ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})))
53	52	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) = ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})))
54		fnsnfv 6258	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 Fn 𝐾 ∧ 𝑥 ∈ 𝐾) → {(𝐺‘𝑥)} = (𝐺 “ {𝑥}))
55	32, 54	sylan 488	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → {(𝐺‘𝑥)} = (𝐺 “ {𝑥}))
56	55	difeq2d 3728	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ((𝐺 “ 𝐾) ∖ {(𝐺‘𝑥)}) = ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})))
57		imassrn 5477	. . . . . . . . . . . . . . 15 ⊢ (𝐺 “ 𝐾) ⊆ ran 𝐺
58	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → 𝐺:𝐾⟶dom 𝐹)
59		frn 6053	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐾⟶dom 𝐹 → ran 𝐺 ⊆ dom 𝐹)
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ran 𝐺 ⊆ dom 𝐹)
61	57, 60	syl5ss 3614	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → (𝐺 “ 𝐾) ⊆ dom 𝐹)
62	61	ssdifd 3746	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ((𝐺 “ 𝐾) ∖ {(𝐺‘𝑥)}) ⊆ (dom 𝐹 ∖ {(𝐺‘𝑥)}))
63	56, 62	eqsstr3d 3640	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ((𝐺 “ 𝐾) ∖ (𝐺 “ {𝑥})) ⊆ (dom 𝐹 ∖ {(𝐺‘𝑥)}))
64	53, 63	eqsstrd 3639	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) ⊆ (dom 𝐹 ∖ {(𝐺‘𝑥)}))
65		imass2 5501	. . . . . . . . . . 11 ⊢ ((𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) ⊆ (dom 𝐹 ∖ {(𝐺‘𝑥)}) → (𝐹 “ (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ⊆ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → (𝐹 “ (𝐺 “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ⊆ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))
67	44, 66	syl5eqss 3649	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) ⊆ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))
68	1, 25	lspss 18984	. . . . . . . . 9 ⊢ ((𝑊 ∈ LMod ∧ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})) ⊆ (Base‘𝑊) ∧ ((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥})) ⊆ (𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))) → ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))))
69	38, 43, 67, 68	syl3anc 1326	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ 𝐾) → ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))))
70	17, 69	syldan 487	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)}))))
71	70	sseld 3602	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → ((𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) → (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))))
72	37, 71	sylbid 230	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ 𝑥 ∈ dom (𝐹 ∘ 𝐺)) → ((𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) → (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))))
73	72	adantrr 753	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))) → (𝑘( ·_𝑠 ‘𝑊)(𝐹‘(𝐺‘𝑥))) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {(𝐺‘𝑥)})))))
74	30, 73	mtod 189	. . 3 ⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) ∧ (𝑥 ∈ dom (𝐹 ∘ 𝐺) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))))
75	74	ralrimivva 2971	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))))
76		simp1 1061	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝑊 ∈ LMod)
77		rellindf 20147	. . . . . 6 ⊢ Rel LIndF
78	77	brrelexi 5158	. . . . 5 ⊢ (𝐹 LIndF 𝑊 → 𝐹 ∈ V)
79	78	3ad2ant2 1083	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐹 ∈ V)
80		simp3 1063	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐺:𝐾–1-1→dom 𝐹)
81		dmexg 7097	. . . . . . 7 ⊢ (𝐹 ∈ V → dom 𝐹 ∈ V)
82	79, 81	syl 17	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → dom 𝐹 ∈ V)
83		f1dmex 7136	. . . . . 6 ⊢ ((𝐺:𝐾–1-1→dom 𝐹 ∧ dom 𝐹 ∈ V) → 𝐾 ∈ V)
84	80, 82, 83	syl2anc 693	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐾 ∈ V)
85		fex 6490	. . . . 5 ⊢ ((𝐺:𝐾⟶dom 𝐹 ∧ 𝐾 ∈ V) → 𝐺 ∈ V)
86	6, 84, 85	syl2anc 693	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → 𝐺 ∈ V)
87		coexg 7117	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘ 𝐺) ∈ V)
88	79, 86, 87	syl2anc 693	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺) ∈ V)
89	1, 24, 25, 26, 28, 27	islindf 20151	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝐹 ∘ 𝐺) ∈ V) → ((𝐹 ∘ 𝐺) LIndF 𝑊 ↔ ((𝐹 ∘ 𝐺):dom (𝐹 ∘ 𝐺)⟶(Base‘𝑊) ∧ ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))))))
90	76, 88, 89	syl2anc 693	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → ((𝐹 ∘ 𝐺) LIndF 𝑊 ↔ ((𝐹 ∘ 𝐺):dom (𝐹 ∘ 𝐺)⟶(Base‘𝑊) ∧ ∀𝑥 ∈ dom (𝐹 ∘ 𝐺)∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)((𝐹 ∘ 𝐺)‘𝑥)) ∈ ((LSpan‘𝑊)‘((𝐹 ∘ 𝐺) “ (dom (𝐹 ∘ 𝐺) ∖ {𝑥}))))))
91	11, 75, 90	mpbir2and 957	1 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺:𝐾–1-1→dom 𝐹) → (𝐹 ∘ 𝐺) LIndF 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 Vcvv 3200 ∖ cdif 3571 ⊆ wss 3574 {csn 4177 class class class wbr 4653 ^◡ccnv 5113 dom cdm 5114 ran crn 5115 “ cima 5117 ∘ ccom 5118 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –1-1→wf1 5885 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 Scalarcsca 15944 ·_𝑠 cvsca 15945 0_gc0g 16100 LModclmod 18863 LSpanclspn 18971 LIndF clindf 20143

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-slot 15861 df-base 15863 df-0g 16102 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-grp 17425 df-lmod 18865 df-lss 18933 df-lsp 18972 df-lindf 20145

This theorem is referenced by: lindfres 20162 f1linds 20164

W3C validator