Metamath Proof Explorer

Theorem lindsenlbs

Description: A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion lindsenlbs ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) )
2 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 eqid ⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
4 3 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
5 2 4 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
6 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
7 6 linds1 ⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
8 eqid ⊢ ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) )
9 6 8 lspssv ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
10 5 7 9 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
11 10 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
12 11 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
13 bren2 ⊢ ( 𝑋 ≈ 𝐼 ↔ ( 𝑋 ≼ 𝐼 ∧ ¬ 𝑋 ≺ 𝐼 ) )
14 13 simprbi ⊢ ( 𝑋 ≈ 𝐼 → ¬ 𝑋 ≺ 𝐼 )
15 snfi ⊢ { 𝑦 } ∈ Fin
16 simp2 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝐼 ∈ Fin )
17 lindsdom ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ≼ 𝐼 )
18 domfi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑋 ≼ 𝐼 ) → 𝑋 ∈ Fin )
19 16 17 18 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ∈ Fin )
20 unfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝑋 ∈ Fin ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
21 15 19 20 sylancr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
22 21 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
23 vex ⊢ 𝑦 ∈ V
24 23 snss ⊢ ( 𝑦 ∈ 𝑋 ↔ { 𝑦 } ⊆ 𝑋 )
25 6 8 lspssid ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
26 5 7 25 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
27 26 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
28 27 sseld ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑦 ∈ 𝑋 → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
29 24 28 syl5bir ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ⊆ 𝑋 → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
30 29 con3dimp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ { 𝑦 } ⊆ 𝑋 )
31 nsspssun ⊢ ( ¬ { 𝑦 } ⊆ 𝑋 ↔ 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) )
32 30 31 sylib ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) )
33 php3 ⊢ ( ( ( { 𝑦 } ∪ 𝑋 ) ∈ Fin ∧ 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
34 22 32 33 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
35 34 adantrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
36 simpl1 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑅 ∈ DivRing )
37 simpl2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝐼 ∈ Fin )
38 snssi ⊢ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
39 38 adantr ⊢ ( ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
40 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
41 unss ⊢ ( ( { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
42 41 biimpi ⊢ ( ( { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
43 39 40 42 syl2anr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
44 simpr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
45 28 con3dimp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ 𝑋 )
46 difsn ⊢ ( ¬ 𝑦 ∈ 𝑋 → ( 𝑋 ∖ { 𝑦 } ) = 𝑋 )
47 45 46 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑋 ∖ { 𝑦 } ) = 𝑋 )
48 47 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
49 44 48 neleqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
50 49 adantlr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
51 difsnid ⊢ ( 𝑧 ∈ 𝑋 → ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑋 )
52 51 fveq2d ⊢ ( 𝑧 ∈ 𝑋 → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
53 52 eleq2d ⊢ ( 𝑧 ∈ 𝑋 → ( 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ↔ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
54 53 notbid ⊢ ( 𝑧 ∈ 𝑋 → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
55 54 biimparc ⊢ ( ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
56 55 adantll ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
57 3 frlmsca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
58 simpl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ DivRing )
59 57 58 eqeltrrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing )
60 eqid ⊢ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) )
61 60 islvec ⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ↔ ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing ) )
62 5 59 61 sylanbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
63 62 3adant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
64 63 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
65 7 ssdifssd ⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
66 65 3ad2ant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
67 66 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
68 simp-4r ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
69 difundir ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( { 𝑦 } ∖ { 𝑧 } ) ∪ ( 𝑋 ∖ { 𝑧 } ) )
70 69 equncomi ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ ( { 𝑦 } ∖ { 𝑧 } ) )
71 elsni ⊢ ( 𝑧 ∈ { 𝑦 } → 𝑧 = 𝑦 )
72 71 eleq1d ⊢ ( 𝑧 ∈ { 𝑦 } → ( 𝑧 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
73 72 notbid ⊢ ( 𝑧 ∈ { 𝑦 } → ( ¬ 𝑧 ∈ 𝑋 ↔ ¬ 𝑦 ∈ 𝑋 ) )
74 45 73 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑧 ∈ { 𝑦 } → ¬ 𝑧 ∈ 𝑋 ) )
75 74 con2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑧 ∈ 𝑋 → ¬ 𝑧 ∈ { 𝑦 } ) )
76 75 imp ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ { 𝑦 } )
77 difsn ⊢ ( ¬ 𝑧 ∈ { 𝑦 } → ( { 𝑦 } ∖ { 𝑧 } ) = { 𝑦 } )
78 76 77 syl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑦 } ∖ { 𝑧 } ) = { 𝑦 } )
79 78 uneq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑋 ∖ { 𝑧 } ) ∪ ( { 𝑦 } ∖ { 𝑧 } ) ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) )
80 70 79 syl5eq ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) )
81 80 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) )
82 81 eleq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ) )
83 82 adantllr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ) )
84 83 biimpa ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) )
85 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
86 85 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ NzRing )
87 57 86 eqeltrrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing )
88 5 87 jca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) )
89 88 anim1i ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
90 89 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
91 8 60 lindsind2 ⊢ ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
92 91 3expa ⊢ ( ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
93 90 92 sylan ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
94 93 ad5ant14 ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
95 84 94 eldifd ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑧 ∈ ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) ) )
96 eqid ⊢ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) )
97 6 96 8 lspsolv ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ∧ ( ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) ) ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
98 64 67 68 95 97 syl13anc ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
99 56 98 mtand ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
100 99 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
101 ralunb ⊢ ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
102 id ⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
103 sneq ⊢ ( 𝑧 = 𝑦 → { 𝑧 } = { 𝑦 } )
104 103 difeq2d ⊢ ( 𝑧 = 𝑦 → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) )
105 uncom ⊢ ( { 𝑦 } ∪ 𝑋 ) = ( 𝑋 ∪ { 𝑦 } )
106 105 difeq1i ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) = ( ( 𝑋 ∪ { 𝑦 } ) ∖ { 𝑦 } )
107 difun2 ⊢ ( ( 𝑋 ∪ { 𝑦 } ) ∖ { 𝑦 } ) = ( 𝑋 ∖ { 𝑦 } )
108 106 107 eqtri ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) = ( 𝑋 ∖ { 𝑦 } )
109 104 108 eqtrdi ⊢ ( 𝑧 = 𝑦 → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( 𝑋 ∖ { 𝑦 } ) )
110 109 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
111 102 110 eleq12d ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) )
112 111 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) )
113 23 112 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
114 113 anbi1i ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) ↔ ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
115 101 114 bitri ⊢ ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
116 50 100 115 sylanbrc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
117 116 ex ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
118 63 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
119 eldifsn ⊢ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ↔ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) )
120 119 biimpi ⊢ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) )
121 120 adantl ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) )
122 38 7 42 syl2anr ⊢ ( ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
123 122 3ad2antl3 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
124 123 sselda ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
125 124 adantr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
126 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) )
127 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
128 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
129 6 60 126 127 128 8 lspsnvs ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) )
130 118 121 125 129 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) )
131 130 sseq1d ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
132 5 3adant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
133 132 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
134 df-3an ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
135 122 ssdifssd ⊢ ( ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
136 6 96 8 lspcl ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
137 5 135 136 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
138 137 anassrs ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
139 134 138 sylanb ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
140 139 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
141 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
142 141 adantl ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
143 6 60 126 127 lmodvscl ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
144 133 142 125 143 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
145 6 96 8 133 140 144 lspsnel5 ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
146 132 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
147 139 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
148 6 96 8 146 147 124 lspsnel5 ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
149 148 adantr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
150 131 145 149 3bitr4rd ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
151 150 notbid ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
152 151 biimpd ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
153 152 ralrimdva ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
154 153 ralimdva ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
155 117 154 syld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
156 155 impr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
157 ovex ⊢ ( 𝑅 freeLMod 𝐼 ) ∈ V
158 6 126 8 60 127 128 islinds2 ⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ V → ( ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) ) )
159 157 158 ax-mp ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
160 43 156 159 sylanbrc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) )
161 lindsdom ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 )
162 36 37 160 161 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 )
163 sdomdomtr ⊢ ( ( 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) ∧ ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 ) → 𝑋 ≺ 𝐼 )
164 35 162 163 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑋 ≺ 𝐼 )
165 164 stoic1a ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑋 ≺ 𝐼 ) → ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
166 14 165 sylan2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
167 iman ⊢ ( ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ↔ ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
168 166 167 sylibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
169 168 ssrdv ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
170 12 169 eqssd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
171 eqid ⊢ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) )
172 6 171 8 islbs4 ⊢ ( 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
173 1 170 172 sylanbrc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )