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 ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
lindfpropd.2 ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
lindfpropd.3 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( 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 lindfpropd ( 𝜑 → ( 𝑋 LIndF 𝐾𝑋 LIndF 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lindfpropd.1 ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2 lindfpropd.2 ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
3 lindfpropd.3 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
4 lindfpropd.4 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
5 lindfpropd.5 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
6 lindfpropd.6 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
7 lindfpropd.k ( 𝜑𝐾𝑉 )
8 lindfpropd.l ( 𝜑𝐿𝑊 )
9 lindfpropd.x ( 𝜑𝑋𝐴 )
10 3 sneqd ( 𝜑 → { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } = { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } )
11 2 10 difeq12d ( 𝜑 → ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) )
12 11 ad2antrr ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) )
13 simplll ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝜑 )
14 simpr ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) )
15 14 eldifad ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
16 simpr ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) → 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) )
17 16 ffvelrnda ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( 𝑋𝑖 ) ∈ ( Base ‘ 𝐾 ) )
18 17 adantr ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( 𝑋𝑖 ) ∈ ( Base ‘ 𝐾 ) )
19 6 oveqrspc2v ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ ( 𝑋𝑖 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) = ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) )
20 13 15 18 19 syl12anc ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) = ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) )
21 eqidd ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
22 ssidd ( 𝜑 → ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐾 ) )
23 eqidd ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
24 21 1 22 4 5 6 23 2 7 8 lsppropd ( 𝜑 → ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐿 ) )
25 24 fveq1d ( 𝜑 → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) )
26 25 ad3antrrr ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) )
27 20 26 eleq12d ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
28 27 notbid ( ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
29 12 28 raleqbidva ( ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
30 29 ralbidva ( ( 𝜑𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
31 30 pm5.32da ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
32 1 feq3d ( 𝜑 → ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ↔ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ) )
33 32 anbi1d ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
34 31 33 bitrd ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
35 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
36 eqid ( ·𝑠𝐾 ) = ( ·𝑠𝐾 )
37 eqid ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐾 )
38 eqid ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
39 eqid ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
40 eqid ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) )
41 35 36 37 38 39 40 islindf ( ( 𝐾𝑉𝑋𝐴 ) → ( 𝑋 LIndF 𝐾 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
42 7 9 41 syl2anc ( 𝜑 → ( 𝑋 LIndF 𝐾 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐾 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
43 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
44 eqid ( ·𝑠𝐿 ) = ( ·𝑠𝐿 )
45 eqid ( LSpan ‘ 𝐿 ) = ( LSpan ‘ 𝐿 )
46 eqid ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
47 eqid ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
48 eqid ( 0g ‘ ( Scalar ‘ 𝐿 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) )
49 43 44 45 46 47 48 islindf ( ( 𝐿𝑊𝑋𝐴 ) → ( 𝑋 LIndF 𝐿 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
50 8 9 49 syl2anc ( 𝜑 → ( 𝑋 LIndF 𝐿 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠𝐿 ) ( 𝑋𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
51 34 42 50 3bitr4d ( 𝜑 → ( 𝑋 LIndF 𝐾𝑋 LIndF 𝐿 ) )