Metamath Proof Explorer

Theorem lindfpropd

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

Ref Expression
Hypotheses lindfpropd.1 ⊢φ→BaseK=BaseL
lindfpropd.2 ⊢φ→BaseScalar⁡K=BaseScalar⁡L
lindfpropd.3 ⊢φ→0Scalar⁡K=0Scalar⁡L
lindfpropd.4 ⊢φ∧x∈BaseK∧y∈BaseK→x+Ky=x+Ly
lindfpropd.5 ⊢φ∧x∈BaseScalar⁡K∧y∈BaseK→x⋅Ky∈BaseK
lindfpropd.6 ⊢φ∧x∈BaseScalar⁡K∧y∈BaseK→x⋅Ky=x⋅Ly
lindfpropd.k ⊢φ→K∈V
lindfpropd.l ⊢φ→L∈W
lindfpropd.x ⊢φ→X∈A
Assertion lindfpropd ⊢φ→XLIndFK↔XLIndFL

Proof

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