Metamath Proof Explorer

Theorem lindfpropd

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

Ref Expression
Hypotheses lindfpropd.1 ⊢ φ → Base K = Base L
lindfpropd.2 ⊢ φ → Base Scalar ⁡ K = Base Scalar ⁡ L
lindfpropd.3 ⊢ φ → 0 Scalar ⁡ K = 0 Scalar ⁡ L
lindfpropd.4 ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x + K y = x + L y
lindfpropd.5 ⊢ φ ∧ x ∈ Base Scalar ⁡ K ∧ y ∈ Base K → x ⋅ K y ∈ Base K
lindfpropd.6 ⊢ φ ∧ x ∈ Base Scalar ⁡ K ∧ y ∈ Base K → x ⋅ K y = x ⋅ L y
lindfpropd.k ⊢ φ → K ∈ V
lindfpropd.l ⊢ φ → L ∈ W
lindfpropd.x ⊢ φ → X ∈ A
Assertion lindfpropd ⊢ φ → X LIndF K ↔ X LIndF L

Proof

Step Hyp Ref Expression
1 lindfpropd.1 ⊢ φ → Base K = Base L
2 lindfpropd.2 ⊢ φ → Base Scalar ⁡ K = Base Scalar ⁡ L
3 lindfpropd.3 ⊢ φ → 0 Scalar ⁡ K = 0 Scalar ⁡ L
4 lindfpropd.4 ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x + K y = x + L y
5 lindfpropd.5 ⊢ φ ∧ x ∈ Base Scalar ⁡ K ∧ y ∈ Base K → x ⋅ K y ∈ Base K
6 lindfpropd.6 ⊢ φ ∧ x ∈ Base Scalar ⁡ K ∧ y ∈ Base K → x ⋅ K y = x ⋅ L y
7 lindfpropd.k ⊢ φ → K ∈ V
8 lindfpropd.l ⊢ φ → L ∈ W
9 lindfpropd.x ⊢ φ → X ∈ A
10 3 sneqd ⊢ φ → 0 Scalar ⁡ K = 0 Scalar ⁡ L
11 2 10 difeq12d ⊢ φ → Base Scalar ⁡ K ∖ 0 Scalar ⁡ K = Base Scalar ⁡ L ∖ 0 Scalar ⁡ L
12 11 ad2antrr ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X → Base Scalar ⁡ K ∖ 0 Scalar ⁡ K = Base Scalar ⁡ L ∖ 0 Scalar ⁡ L
13 simplll ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → φ
14 simpr ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K
15 14 eldifad ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → k ∈ Base Scalar ⁡ K
16 simpr ⊢ φ ∧ X : dom ⁡ X ⟶ Base K → X : dom ⁡ X ⟶ Base K
17 16 ffvelrnda ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X → X ⁡ i ∈ Base K
18 17 adantr ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → X ⁡ i ∈ Base K
19 6 oveqrspc2v ⊢ φ ∧ k ∈ Base Scalar ⁡ K ∧ X ⁡ i ∈ Base K → k ⋅ K X ⁡ i = k ⋅ L X ⁡ i
20 13 15 18 19 syl12anc ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → k ⋅ K X ⁡ i = k ⋅ L X ⁡ i
21 eqidd ⊢ φ → Base K = Base K
22 ssidd ⊢ φ → Base K ⊆ Base K
23 eqidd ⊢ φ → Base Scalar ⁡ K = Base Scalar ⁡ K
24 21 1 22 4 5 6 23 2 7 8 lsppropd ⊢ φ → LSpan ⁡ K = LSpan ⁡ L
25 24 fveq1d ⊢ φ → LSpan ⁡ K ⁡ X dom ⁡ X ∖ i = LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
26 25 ad3antrrr ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → LSpan ⁡ K ⁡ X dom ⁡ X ∖ i = LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
27 20 26 eleq12d ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
28 27 notbid ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X ∧ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K → ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
29 12 28 raleqbidva ⊢ φ ∧ X : dom ⁡ X ⟶ Base K ∧ i ∈ dom ⁡ X → ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
30 29 ralbidva ⊢ φ ∧ X : dom ⁡ X ⟶ Base K → ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
31 30 pm5.32da ⊢ φ → X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
32 1 feq3d ⊢ φ → X : dom ⁡ X ⟶ Base K ↔ X : dom ⁡ X ⟶ Base L
33 32 anbi1d ⊢ φ → X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i ↔ X : dom ⁡ X ⟶ Base L ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
34 31 33 bitrd ⊢ φ → X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i ↔ X : dom ⁡ X ⟶ Base L ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
35 eqid ⊢ Base K = Base K
36 eqid ⊢ ⋅ K = ⋅ K
37 eqid ⊢ LSpan ⁡ K = LSpan ⁡ K
38 eqid ⊢ Scalar ⁡ K = Scalar ⁡ K
39 eqid ⊢ Base Scalar ⁡ K = Base Scalar ⁡ K
40 eqid ⊢ 0 Scalar ⁡ K = 0 Scalar ⁡ K
41 35 36 37 38 39 40 islindf ⊢ K ∈ V ∧ X ∈ A → X LIndF K ↔ X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i
42 7 9 41 syl2anc ⊢ φ → X LIndF K ↔ X : dom ⁡ X ⟶ Base K ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ K ∖ 0 Scalar ⁡ K ¬ k ⋅ K X ⁡ i ∈ LSpan ⁡ K ⁡ X dom ⁡ X ∖ i
43 eqid ⊢ Base L = Base L
44 eqid ⊢ ⋅ L = ⋅ L
45 eqid ⊢ LSpan ⁡ L = LSpan ⁡ L
46 eqid ⊢ Scalar ⁡ L = Scalar ⁡ L
47 eqid ⊢ Base Scalar ⁡ L = Base Scalar ⁡ L
48 eqid ⊢ 0 Scalar ⁡ L = 0 Scalar ⁡ L
49 43 44 45 46 47 48 islindf ⊢ L ∈ W ∧ X ∈ A → X LIndF L ↔ X : dom ⁡ X ⟶ Base L ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
50 8 9 49 syl2anc ⊢ φ → X LIndF L ↔ X : dom ⁡ X ⟶ Base L ∧ ∀ i ∈ dom ⁡ X ∀ k ∈ Base Scalar ⁡ L ∖ 0 Scalar ⁡ L ¬ k ⋅ L X ⁡ i ∈ LSpan ⁡ L ⁡ X dom ⁡ X ∖ i
51 34 42 50 3bitr4d ⊢ φ → X LIndF K ↔ X LIndF L