This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lindfmm

Description: Linear independence of a family is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses lindfmm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
Assertion lindfmm ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑆 ↔ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lindfmm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 rellindf ⊢ Rel LIndF
4 3 brrelex1i ⊢ ( 𝐹 LIndF 𝑆 → 𝐹 ∈ V )
5 simp3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
6 dmfex ⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ V )
7 4 5 6 syl2anr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝐹 LIndF 𝑆 ) → 𝐼 ∈ V )
8 7 ex ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑆 → 𝐼 ∈ V ) )
9 3 brrelex1i ⊢ ( ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 → ( 𝐺 ∘ 𝐹 ) ∈ V )
10 f1f ⊢ ( 𝐺 : 𝐵 –1-1→ 𝐶 → 𝐺 : 𝐵 ⟶ 𝐶 )
11 fco ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 )
12 10 11 sylan ⊢ ( ( 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 )
13 12 3adant1 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 )
14 dmfex ⊢ ( ( ( 𝐺 ∘ 𝐹 ) ∈ V ∧ ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 ) → 𝐼 ∈ V )
15 9 13 14 syl2anr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) → 𝐼 ∈ V )
16 15 ex ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 → 𝐼 ∈ V ) )
17 eldifi ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
18 simpllr ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → 𝐺 : 𝐵 –1-1→ 𝐶 )
19 lmhmlmod1 ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
20 19 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → 𝑆 ∈ LMod )
21 simprr ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
22 simprl ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → 𝐹 : 𝐼 ⟶ 𝐵 )
23 simpl ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → 𝑥 ∈ 𝐼 )
24 ffvelcdm ⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
25 22 23 24 syl2an ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
26 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
27 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
28 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
29 1 26 27 28 lmodvscl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐵 )
30 20 21 25 29 syl3anc ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐵 )
31 imassrn ⊢ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ran 𝐹
32 frn ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
33 32 adantr ⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) → ran 𝐹 ⊆ 𝐵 )
34 31 33 sstrid ⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) → ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝐵 )
35 34 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝐵 )
36 eqid ⊢ ( LSpan ‘ 𝑆 ) = ( LSpan ‘ 𝑆 )
37 1 36 lspssv ⊢ ( ( 𝑆 ∈ LMod ∧ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝐵 ) → ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ 𝐵 )
38 20 35 37 syl2anc ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ 𝐵 )
39 f1elima ⊢ ( ( 𝐺 : 𝐵 –1-1→ 𝐶 ∧ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐵 ∧ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ 𝐵 ) → ( ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
40 18 30 38 39 syl3anc ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
41 simplll ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) )
42 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
43 26 28 1 27 42 lmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
44 41 21 25 43 syl3anc ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
45 ffn ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → 𝐹 Fn 𝐼 )
46 45 ad2antrl ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → 𝐹 Fn 𝐼 )
47 fvco2 ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
48 46 23 47 syl2an ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
49 48 oveq2d ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
50 44 49 eqtr4d ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) )
51 eqid ⊢ ( LSpan ‘ 𝑇 ) = ( LSpan ‘ 𝑇 )
52 1 36 51 lmhmlsp ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝐵 ) → ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐺 “ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
53 41 35 52 syl2anc ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐺 “ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
54 imaco ⊢ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝐺 “ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) )
55 54 fveq2i ⊢ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( 𝐺 “ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
56 53 55 eqtr4di ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
57 50 56 eleq12d ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ( 𝐺 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( 𝐺 “ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
58 40 57 bitr3d ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
59 58 notbid ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
60 59 anassrs ⊢ ( ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
61 17 60 sylan2 ⊢ ( ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
62 61 ralbidva ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
63 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
64 26 63 lmhmsca ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
65 64 fveq2d ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
66 64 fveq2d ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑆 ) ) )
67 66 sneqd ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } = { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } )
68 65 67 difeq12d ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) )
69 68 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) )
70 69 raleqdv ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
71 62 70 bitr4d ⊢ ( ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
72 71 ralbidva ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
73 19 ad2antrr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → 𝑆 ∈ LMod )
74 simprr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → 𝐼 ∈ V )
75 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑆 ) ) = ( 0g ‘ ( Scalar ‘ 𝑆 ) )
76 1 27 36 26 28 75 islindf2 ⊢ ( ( 𝑆 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑆 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
77 73 74 22 76 syl3anc ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → ( 𝐹 LIndF 𝑆 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑆 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑆 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
78 lmhmlmod2 ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
79 78 ad2antrr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → 𝑇 ∈ LMod )
80 12 ad2ant2lr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 )
81 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
82 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) )
83 2 42 51 63 81 82 islindf2 ⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ V ∧ ( 𝐺 ∘ 𝐹 ) : 𝐼 ⟶ 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
84 79 74 80 83 syl3anc ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → ( ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑇 ) ‘ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
85 72 77 84 3bitr4d ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) ∧ ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ V ) ) → ( 𝐹 LIndF 𝑆 ↔ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) )
86 85 exp32 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ) → ( 𝐹 : 𝐼 ⟶ 𝐵 → ( 𝐼 ∈ V → ( 𝐹 LIndF 𝑆 ↔ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) ) ) )
87 86 3impia ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐼 ∈ V → ( 𝐹 LIndF 𝑆 ↔ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) ) )
88 8 16 87 pm5.21ndd ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑆 ↔ ( 𝐺 ∘ 𝐹 ) LIndF 𝑇 ) )