lindfpropd - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lindfpropd		Structured version Visualization version GIF version

Theorem lindfpropd 32772

Description: Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.)

**Hypotheses**
Ref	Expression
lindfpropd.1	⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))
lindfpropd.2	⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿)))
lindfpropd.3	⊢ (𝜑 → (0_g‘(Scalar‘𝐾)) = (0_g‘(Scalar‘𝐿)))
lindfpropd.4	⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
lindfpropd.5	⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·_𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾))
lindfpropd.6	⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·_𝑠 ‘𝐾)𝑦) = (𝑥( ·_𝑠 ‘𝐿)𝑦))
lindfpropd.k	⊢ (𝜑 → 𝐾 ∈ 𝑉)
lindfpropd.l	⊢ (𝜑 → 𝐿 ∈ 𝑊)
lindfpropd.x	⊢ (𝜑 → 𝑋 ∈ 𝐴)

**Assertion**
Ref	Expression
lindfpropd	⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿))

Distinct variable groups: 𝑥,𝐾,𝑦 𝑥,𝐿,𝑦 𝑥,𝑋,𝑦 𝜑,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑥,𝑦) 𝑉(𝑥,𝑦) 𝑊(𝑥,𝑦)

Proof of Theorem lindfpropd Dummy variables 𝑖 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lindfpropd.2	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿)))
2		lindfpropd.3	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘(Scalar‘𝐾)) = (0_g‘(Scalar‘𝐿)))
3	2	sneqd 4639	. . . . . . . 8 ⊢ (𝜑 → {(0_g‘(Scalar‘𝐾))} = {(0_g‘(Scalar‘𝐿))})
4	1, 3	difeq12d 4122	. . . . . . 7 ⊢ (𝜑 → ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) = ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}))
5	4	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) → ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) = ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}))
6		simplll 771	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → 𝜑)
7		simpr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}))
8	7	eldifad 3959	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → 𝑘 ∈ (Base‘(Scalar‘𝐾)))
9		simpr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) → 𝑋:dom 𝑋⟶(Base‘𝐾))
10	9	ffvelcdmda 7085	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) → (𝑋‘𝑖) ∈ (Base‘𝐾))
11	10	adantr 479	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → (𝑋‘𝑖) ∈ (Base‘𝐾))
12		lindfpropd.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·_𝑠 ‘𝐾)𝑦) = (𝑥( ·_𝑠 ‘𝐿)𝑦))
13	12	oveqrspc2v 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝐾)) ∧ (𝑋‘𝑖) ∈ (Base‘𝐾))) → (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) = (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)))
14	6, 8, 11, 13	syl12anc 833	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) = (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)))
15		eqidd 2731	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐾))
16		lindfpropd.1	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))
17		ssidd 4004	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐾) ⊆ (Base‘𝐾))
18		lindfpropd.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
19		lindfpropd.5	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·_𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾))
20		eqidd 2731	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐾)))
21		lindfpropd.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ 𝑉)
22		lindfpropd.l	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ 𝑊)
23	15, 16, 17, 18, 19, 12, 20, 1, 21, 22	lsppropd 20773	. . . . . . . . . 10 ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿))
24	23	fveq1d 6892	. . . . . . . . 9 ⊢ (𝜑 → ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) = ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))
25	24	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) = ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))
26	14, 25	eleq12d 2825	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → ((𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) ↔ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))))
27	26	notbid 317	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))})) → (¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) ↔ ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))))
28	5, 27	raleqbidva 3325	. . . . 5 ⊢ (((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) ∧ 𝑖 ∈ dom 𝑋) → (∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))))
29	28	ralbidva 3173	. . . 4 ⊢ ((𝜑 ∧ 𝑋:dom 𝑋⟶(Base‘𝐾)) → (∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))) ↔ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))))
30	29	pm5.32da 577	. . 3 ⊢ (𝜑 → ((𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))) ↔ (𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
31	16	feq3d 6703	. . . 4 ⊢ (𝜑 → (𝑋:dom 𝑋⟶(Base‘𝐾) ↔ 𝑋:dom 𝑋⟶(Base‘𝐿)))
32	31	anbi1d 628	. . 3 ⊢ (𝜑 → ((𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))) ↔ (𝑋:dom 𝑋⟶(Base‘𝐿) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
33	30, 32	bitrd 278	. 2 ⊢ (𝜑 → ((𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖})))) ↔ (𝑋:dom 𝑋⟶(Base‘𝐿) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
34		lindfpropd.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
35		eqid 2730	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
36		eqid 2730	. . . 4 ⊢ ( ·_𝑠 ‘𝐾) = ( ·_𝑠 ‘𝐾)
37		eqid 2730	. . . 4 ⊢ (LSpan‘𝐾) = (LSpan‘𝐾)
38		eqid 2730	. . . 4 ⊢ (Scalar‘𝐾) = (Scalar‘𝐾)
39		eqid 2730	. . . 4 ⊢ (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐾))
40		eqid 2730	. . . 4 ⊢ (0_g‘(Scalar‘𝐾)) = (0_g‘(Scalar‘𝐾))
41	35, 36, 37, 38, 39, 40	islindf 21586	. . 3 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → (𝑋 LIndF 𝐾 ↔ (𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
42	21, 34, 41	syl2anc 582	. 2 ⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ (𝑋:dom 𝑋⟶(Base‘𝐾) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐾)) ∖ {(0_g‘(Scalar‘𝐾))}) ¬ (𝑘( ·_𝑠 ‘𝐾)(𝑋‘𝑖)) ∈ ((LSpan‘𝐾)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
43		eqid 2730	. . . 4 ⊢ (Base‘𝐿) = (Base‘𝐿)
44		eqid 2730	. . . 4 ⊢ ( ·_𝑠 ‘𝐿) = ( ·_𝑠 ‘𝐿)
45		eqid 2730	. . . 4 ⊢ (LSpan‘𝐿) = (LSpan‘𝐿)
46		eqid 2730	. . . 4 ⊢ (Scalar‘𝐿) = (Scalar‘𝐿)
47		eqid 2730	. . . 4 ⊢ (Base‘(Scalar‘𝐿)) = (Base‘(Scalar‘𝐿))
48		eqid 2730	. . . 4 ⊢ (0_g‘(Scalar‘𝐿)) = (0_g‘(Scalar‘𝐿))
49	43, 44, 45, 46, 47, 48	islindf 21586	. . 3 ⊢ ((𝐿 ∈ 𝑊 ∧ 𝑋 ∈ 𝐴) → (𝑋 LIndF 𝐿 ↔ (𝑋:dom 𝑋⟶(Base‘𝐿) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
50	22, 34, 49	syl2anc 582	. 2 ⊢ (𝜑 → (𝑋 LIndF 𝐿 ↔ (𝑋:dom 𝑋⟶(Base‘𝐿) ∧ ∀𝑖 ∈ dom 𝑋∀𝑘 ∈ ((Base‘(Scalar‘𝐿)) ∖ {(0_g‘(Scalar‘𝐿))}) ¬ (𝑘( ·_𝑠 ‘𝐿)(𝑋‘𝑖)) ∈ ((LSpan‘𝐿)‘(𝑋 “ (dom 𝑋 ∖ {𝑖}))))))
51	33, 42, 50	3bitr4d 310	1 ⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ∀wral 3059 ∖ cdif 3944 {csn 4627 class class class wbr 5147 dom cdm 5675 “ cima 5678 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 Basecbs 17148 +_gcplusg 17201 Scalarcsca 17204 ·_𝑠 cvsca 17205 0_gc0g 17389 LSpanclspn 20726 LIndF clindf 21578

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-lss 20687 df-lsp 20727 df-lindf 21580

This theorem is referenced by: lindspropd 32773

W3C validator