Metamath Proof Explorer

Theorem f1lindf

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion f1lindf ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) LIndF 𝑊 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 1 lindff ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
3 2 ancoms ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
4 3 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
5 f1f ⊢ ( 𝐺 : 𝐾 –1-1→ dom 𝐹 → 𝐺 : 𝐾 ⟶ dom 𝐹 )
6 5 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐺 : 𝐾 ⟶ dom 𝐹 )
7 fco ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : 𝐾 ⟶ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) : 𝐾 ⟶ ( Base ‘ 𝑊 ) )
8 4 6 7 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) : 𝐾 ⟶ ( Base ‘ 𝑊 ) )
9 8 ffdmd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ( Base ‘ 𝑊 ) )
10 simpl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝐹 LIndF 𝑊 )
11 6 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → 𝐺 : 𝐾 ⟶ dom 𝐹 )
12 8 fdmd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → dom ( 𝐹 ∘ 𝐺 ) = 𝐾 )
13 12 eleq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ 𝑥 ∈ 𝐾 ) )
14 13 biimpa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → 𝑥 ∈ 𝐾 )
15 11 14 ffvelrnd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ dom 𝐹 )
16 15 adantrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ dom 𝐹 )
17 eldifi ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 17 ad2antll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 eldifsni ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
20 19 ad2antll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
21 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
22 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
23 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
24 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
25 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
26 21 22 23 24 25 lindfind ⊢ ( ( ( 𝐹 LIndF 𝑊 ∧ ( 𝐺 ‘ 𝑥 ) ∈ dom 𝐹 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) )
27 10 16 18 20 26 syl22anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) )
28 f1fn ⊢ ( 𝐺 : 𝐾 –1-1→ dom 𝐹 → 𝐺 Fn 𝐾 )
29 28 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐺 Fn 𝐾 )
30 29 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → 𝐺 Fn 𝐾 )
31 fvco2 ⊢ ( ( 𝐺 Fn 𝐾 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
32 30 14 31 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
33 32 oveq2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
34 33 eleq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ) )
35 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑊 ∈ LMod )
36 imassrn ⊢ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ⊆ ran 𝐹
37 4 frnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ran 𝐹 ⊆ ( Base ‘ 𝑊 ) )
38 36 37 sstrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ⊆ ( Base ‘ 𝑊 ) )
39 38 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ⊆ ( Base ‘ 𝑊 ) )
40 imaco ⊢ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) = ( 𝐹 “ ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) )
41 12 difeq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) = ( 𝐾 ∖ { 𝑥 } ) )
42 41 imaeq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) = ( 𝐺 “ ( 𝐾 ∖ { 𝑥 } ) ) )
43 df-f1 ⊢ ( 𝐺 : 𝐾 –1-1→ dom 𝐹 ↔ ( 𝐺 : 𝐾 ⟶ dom 𝐹 ∧ Fun ◡ 𝐺 ) )
44 43 simprbi ⊢ ( 𝐺 : 𝐾 –1-1→ dom 𝐹 → Fun ◡ 𝐺 )
45 44 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → Fun ◡ 𝐺 )
46 imadif ⊢ ( Fun ◡ 𝐺 → ( 𝐺 “ ( 𝐾 ∖ { 𝑥 } ) ) = ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) )
47 45 46 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐺 “ ( 𝐾 ∖ { 𝑥 } ) ) = ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) )
48 42 47 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) = ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) )
49 48 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) = ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) )
50 fnsnfv ⊢ ( ( 𝐺 Fn 𝐾 ∧ 𝑥 ∈ 𝐾 ) → { ( 𝐺 ‘ 𝑥 ) } = ( 𝐺 “ { 𝑥 } ) )
51 29 50 sylan ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → { ( 𝐺 ‘ 𝑥 ) } = ( 𝐺 “ { 𝑥 } ) )
52 51 difeq2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐺 “ 𝐾 ) ∖ { ( 𝐺 ‘ 𝑥 ) } ) = ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) )
53 imassrn ⊢ ( 𝐺 “ 𝐾 ) ⊆ ran 𝐺
54 6 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐺 : 𝐾 ⟶ dom 𝐹 )
55 54 frnd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ran 𝐺 ⊆ dom 𝐹 )
56 53 55 sstrid ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐺 “ 𝐾 ) ⊆ dom 𝐹 )
57 56 ssdifd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐺 “ 𝐾 ) ∖ { ( 𝐺 ‘ 𝑥 ) } ) ⊆ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) )
58 52 57 eqsstrrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐺 “ 𝐾 ) ∖ ( 𝐺 “ { 𝑥 } ) ) ⊆ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) )
59 49 58 eqsstrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ⊆ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) )
60 imass2 ⊢ ( ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ⊆ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) → ( 𝐹 “ ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) )
61 59 60 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐹 “ ( 𝐺 “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) )
62 40 61 eqsstrid ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) )
63 1 22 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ⊆ ( Base ‘ 𝑊 ) ∧ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) )
64 35 39 62 63 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) )
65 14 64 syldan ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) )
66 65 sseld ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) ) )
67 34 66 sylbid ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) ) )
68 67 adantrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { ( 𝐺 ‘ 𝑥 ) } ) ) ) ) )
69 27 68 mtod ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) ∧ ( 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) )
70 69 ralrimivva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ∀ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) )
71 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝑊 ∈ LMod )
72 rellindf ⊢ Rel LIndF
73 72 brrelex1i ⊢ ( 𝐹 LIndF 𝑊 → 𝐹 ∈ V )
74 73 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐹 ∈ V )
75 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐺 : 𝐾 –1-1→ dom 𝐹 )
76 74 dmexd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → dom 𝐹 ∈ V )
77 f1dmex ⊢ ( ( 𝐺 : 𝐾 –1-1→ dom 𝐹 ∧ dom 𝐹 ∈ V ) → 𝐾 ∈ V )
78 75 76 77 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐾 ∈ V )
79 6 78 fexd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → 𝐺 ∈ V )
80 coexg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
81 74 79 80 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
82 1 21 22 23 25 24 islindf ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 ∘ 𝐺 ) ∈ V ) → ( ( 𝐹 ∘ 𝐺 ) LIndF 𝑊 ↔ ( ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ) ) )
83 71 81 82 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( ( 𝐹 ∘ 𝐺 ) LIndF 𝑊 ↔ ( ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ∘ 𝐺 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ∘ 𝐺 ) “ ( dom ( 𝐹 ∘ 𝐺 ) ∖ { 𝑥 } ) ) ) ) ) )
84 9 70 83 mpbir2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ 𝐺 : 𝐾 –1-1→ dom 𝐹 ) → ( 𝐹 ∘ 𝐺 ) LIndF 𝑊 )