Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldepspr Structured version   Visualization version   GIF version

Theorem ldepspr 42056
 Description: If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.)
Hypotheses
Ref Expression
snlindsntor.b 𝐵 = (Base‘𝑀)
snlindsntor.r 𝑅 = (Scalar‘𝑀)
snlindsntor.s 𝑆 = (Base‘𝑅)
snlindsntor.0 0 = (0g𝑅)
snlindsntor.z 𝑍 = (0g𝑀)
snlindsntor.t · = ( ·𝑠𝑀)
Assertion
Ref Expression
ldepspr ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀))

Proof of Theorem ldepspr
Dummy variables 𝑓 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3simpa 1051 . . . . . . 7 ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑋𝐵𝑌𝐵))
21ad2antlr 759 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑋𝐵𝑌𝐵))
3 fvex 6113 . . . . . . . 8 (1r𝑅) ∈ V
4 fvex 6113 . . . . . . . 8 ((invg𝑅)‘𝐴) ∈ V
53, 4pm3.2i 470 . . . . . . 7 ((1r𝑅) ∈ V ∧ ((invg𝑅)‘𝐴) ∈ V)
65a1i 11 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((1r𝑅) ∈ V ∧ ((invg𝑅)‘𝐴) ∈ V))
7 simp3 1056 . . . . . . 7 ((𝑋𝐵𝑌𝐵𝑋𝑌) → 𝑋𝑌)
87ad2antlr 759 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝑋𝑌)
9 fprg 6327 . . . . . 6 (((𝑋𝐵𝑌𝐵) ∧ ((1r𝑅) ∈ V ∧ ((invg𝑅)‘𝐴) ∈ V) ∧ 𝑋𝑌) → {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}:{𝑋, 𝑌}⟶{(1r𝑅), ((invg𝑅)‘𝐴)})
102, 6, 8, 9syl3anc 1318 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}:{𝑋, 𝑌}⟶{(1r𝑅), ((invg𝑅)‘𝐴)})
11 prfi 8120 . . . . . 6 {𝑋, 𝑌} ∈ Fin
1211a1i 11 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} ∈ Fin)
13 snlindsntor.0 . . . . . . 7 0 = (0g𝑅)
14 fvex 6113 . . . . . . 7 (0g𝑅) ∈ V
1513, 14eqeltri 2684 . . . . . 6 0 ∈ V
1615a1i 11 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 0 ∈ V)
1710, 12, 16fdmfifsupp 8168 . . . 4 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} finSupp 0 )
187anim2i 591 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → (𝑀 ∈ LMod ∧ 𝑋𝑌))
1918adantr 480 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑀 ∈ LMod ∧ 𝑋𝑌))
20 snlindsntor.r . . . . . . . . 9 𝑅 = (Scalar‘𝑀)
21 snlindsntor.s . . . . . . . . 9 𝑆 = (Base‘𝑅)
22 eqid 2610 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
2320, 21, 22lmod1cl 18713 . . . . . . . 8 (𝑀 ∈ LMod → (1r𝑅) ∈ 𝑆)
24 simp1 1054 . . . . . . . 8 ((𝑋𝐵𝑌𝐵𝑋𝑌) → 𝑋𝐵)
2523, 24anim12ci 589 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → (𝑋𝐵 ∧ (1r𝑅) ∈ 𝑆))
2625adantr 480 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑋𝐵 ∧ (1r𝑅) ∈ 𝑆))
27 simp2 1055 . . . . . . 7 ((𝑋𝐵𝑌𝐵𝑋𝑌) → 𝑌𝐵)
2827ad2antlr 759 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝑌𝐵)
2920lmodfgrp 18695 . . . . . . . 8 (𝑀 ∈ LMod → 𝑅 ∈ Grp)
3029adantr 480 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → 𝑅 ∈ Grp)
31 simpl 472 . . . . . . 7 ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → 𝐴𝑆)
32 eqid 2610 . . . . . . . 8 (invg𝑅) = (invg𝑅)
3321, 32grpinvcl 17290 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐴𝑆) → ((invg𝑅)‘𝐴) ∈ 𝑆)
3430, 31, 33syl2an 493 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((invg𝑅)‘𝐴) ∈ 𝑆)
35 snlindsntor.b . . . . . . 7 𝐵 = (Base‘𝑀)
36 snlindsntor.t . . . . . . 7 · = ( ·𝑠𝑀)
37 eqid 2610 . . . . . . 7 (+g𝑀) = (+g𝑀)
38 eqid 2610 . . . . . . 7 {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}
3935, 20, 21, 36, 37, 38lincvalpr 42001 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑋𝑌) ∧ (𝑋𝐵 ∧ (1r𝑅) ∈ 𝑆) ∧ (𝑌𝐵 ∧ ((invg𝑅)‘𝐴) ∈ 𝑆)) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = (((1r𝑅) · 𝑋)(+g𝑀)(((invg𝑅)‘𝐴) · 𝑌)))
4019, 26, 28, 34, 39syl112anc 1322 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = (((1r𝑅) · 𝑋)(+g𝑀)(((invg𝑅)‘𝐴) · 𝑌)))
41 simpll 786 . . . . . . 7 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝑀 ∈ LMod)
4224ad2antlr 759 . . . . . . . 8 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝑋𝐵)
4331adantl 481 . . . . . . . 8 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝐴𝑆)
4442, 28, 433jca 1235 . . . . . . 7 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑋𝐵𝑌𝐵𝐴𝑆))
4541, 44jca 553 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝐴𝑆)))
46 simprr 792 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → 𝑋 = (𝐴 · 𝑌))
47 snlindsntor.z . . . . . . 7 𝑍 = (0g𝑀)
4835, 20, 21, 13, 47, 36, 22, 32ldepsprlem 42055 . . . . . 6 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝐴𝑆)) → (𝑋 = (𝐴 · 𝑌) → (((1r𝑅) · 𝑋)(+g𝑀)(((invg𝑅)‘𝐴) · 𝑌)) = 𝑍))
4945, 46, 48sylc 63 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (((1r𝑅) · 𝑋)(+g𝑀)(((invg𝑅)‘𝐴) · 𝑌)) = 𝑍)
5040, 49eqtrd 2644 . . . 4 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍)
5120lmodring 18694 . . . . . . . . . 10 (𝑀 ∈ LMod → 𝑅 ∈ Ring)
52 eqcom 2617 . . . . . . . . . . . 12 ((1r𝑅) = (0g𝑅) ↔ (0g𝑅) = (1r𝑅))
53 eqid 2610 . . . . . . . . . . . . . . 15 (0g𝑅) = (0g𝑅)
5421, 53, 2201eq0ring 19093 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (0g𝑅) = (1r𝑅)) → 𝑆 = {(0g𝑅)})
55 sneq 4135 . . . . . . . . . . . . . . . . 17 ((0g𝑅) = (1r𝑅) → {(0g𝑅)} = {(1r𝑅)})
5655eqeq2d 2620 . . . . . . . . . . . . . . . 16 ((0g𝑅) = (1r𝑅) → (𝑆 = {(0g𝑅)} ↔ 𝑆 = {(1r𝑅)}))
57 eleq2 2677 . . . . . . . . . . . . . . . . . . 19 (𝑆 = {(1r𝑅)} → (𝐴𝑆𝐴 ∈ {(1r𝑅)}))
58 elsni 4142 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ {(1r𝑅)} → 𝐴 = (1r𝑅))
59 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 = (1r𝑅) → (𝐴 · 𝑌) = ((1r𝑅) · 𝑌))
6059eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 = (1r𝑅) → (𝑋 = (𝐴 · 𝑌) ↔ 𝑋 = ((1r𝑅) · 𝑌)))
6127anim1i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → (𝑌𝐵𝑀 ∈ LMod))
6261ancomd 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → (𝑀 ∈ LMod ∧ 𝑌𝐵))
6335, 20, 36, 22lmodvs1 18714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ LMod ∧ 𝑌𝐵) → ((1r𝑅) · 𝑌) = 𝑌)
6462, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → ((1r𝑅) · 𝑌) = 𝑌)
6564eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = ((1r𝑅) · 𝑌) ↔ 𝑋 = 𝑌))
66 eqneqall 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 = 𝑌 → (𝑋𝑌 → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
6766com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝑌 → (𝑋 = 𝑌 → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
68673ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑋 = 𝑌 → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
6968adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = 𝑌 → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
7065, 69sylbid 229 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝐵𝑌𝐵𝑋𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = ((1r𝑅) · 𝑌) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
7170ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (𝑋 = ((1r𝑅) · 𝑌) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))
7271com3r 85 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = ((1r𝑅) · 𝑌) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))
7360, 72syl6bi 242 . . . . . . . . . . . . . . . . . . . 20 (𝐴 = (1r𝑅) → (𝑋 = (𝐴 · 𝑌) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
7458, 73syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ {(1r𝑅)} → (𝑋 = (𝐴 · 𝑌) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
7557, 74syl6bi 242 . . . . . . . . . . . . . . . . . 18 (𝑆 = {(1r𝑅)} → (𝐴𝑆 → (𝑋 = (𝐴 · 𝑌) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
7675impd 446 . . . . . . . . . . . . . . . . 17 (𝑆 = {(1r𝑅)} → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
7776com23 84 . . . . . . . . . . . . . . . 16 (𝑆 = {(1r𝑅)} → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
7856, 77syl6bi 242 . . . . . . . . . . . . . . 15 ((0g𝑅) = (1r𝑅) → (𝑆 = {(0g𝑅)} → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
7978adantl 481 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (0g𝑅) = (1r𝑅)) → (𝑆 = {(0g𝑅)} → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
8054, 79mpd 15 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (0g𝑅) = (1r𝑅)) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
8180ex 449 . . . . . . . . . . . 12 (𝑅 ∈ Ring → ((0g𝑅) = (1r𝑅) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
8252, 81syl5bi 231 . . . . . . . . . . 11 (𝑅 ∈ Ring → ((1r𝑅) = (0g𝑅) → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
8382com25 97 . . . . . . . . . 10 (𝑅 ∈ Ring → (𝑀 ∈ LMod → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → ((1r𝑅) = (0g𝑅) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))))))
8451, 83mpcom 37 . . . . . . . . 9 (𝑀 ∈ LMod → ((𝑋𝐵𝑌𝐵𝑋𝑌) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → ((1r𝑅) = (0g𝑅) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))))
8584imp31 447 . . . . . . . 8 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((1r𝑅) = (0g𝑅) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
86 orc 399 . . . . . . . 8 (¬ (1r𝑅) = (0g𝑅) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))
8785, 86pm2.61d1 170 . . . . . . 7 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))
8813eqeq2i 2622 . . . . . . . . 9 ((1r𝑅) = 0 ↔ (1r𝑅) = (0g𝑅))
8988necon3abii 2828 . . . . . . . 8 ((1r𝑅) ≠ 0 ↔ ¬ (1r𝑅) = (0g𝑅))
9089orbi1i 541 . . . . . . 7 (((1r𝑅) ≠ 0 ∨ ((invg𝑅)‘𝐴) ≠ 0 ) ↔ (¬ (1r𝑅) = (0g𝑅) ∨ ((invg𝑅)‘𝐴) ≠ 0 ))
9187, 90sylibr 223 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((1r𝑅) ≠ 0 ∨ ((invg𝑅)‘𝐴) ≠ 0 ))
923a1i 11 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (1r𝑅) ∈ V)
93 fvpr1g 6363 . . . . . . . . 9 ((𝑋𝐵 ∧ (1r𝑅) ∈ V ∧ 𝑋𝑌) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) = (1r𝑅))
9442, 92, 8, 93syl3anc 1318 . . . . . . . 8 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) = (1r𝑅))
9594neeq1d 2841 . . . . . . 7 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ↔ (1r𝑅) ≠ 0 ))
964a1i 11 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((invg𝑅)‘𝐴) ∈ V)
97 fvpr2g 6364 . . . . . . . . 9 ((𝑌𝐵 ∧ ((invg𝑅)‘𝐴) ∈ V ∧ 𝑋𝑌) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) = ((invg𝑅)‘𝐴))
9828, 96, 8, 97syl3anc 1318 . . . . . . . 8 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) = ((invg𝑅)‘𝐴))
9998neeq1d 2841 . . . . . . 7 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 ↔ ((invg𝑅)‘𝐴) ≠ 0 ))
10095, 99orbi12d 742 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ((({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ∨ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 ) ↔ ((1r𝑅) ≠ 0 ∨ ((invg𝑅)‘𝐴) ≠ 0 )))
10191, 100mpbird 246 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ∨ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 ))
102 fveq2 6103 . . . . . . . 8 (𝑣 = 𝑋 → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) = ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋))
103102neeq1d 2841 . . . . . . 7 (𝑣 = 𝑋 → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ))
104 fveq2 6103 . . . . . . . 8 (𝑣 = 𝑌 → ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) = ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌))
105104neeq1d 2841 . . . . . . 7 (𝑣 = 𝑌 → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 ))
106103, 105rexprg 4182 . . . . . 6 ((𝑋𝐵𝑌𝐵) → (∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ↔ (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ∨ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 )))
1072, 106syl 17 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ↔ (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑋) ≠ 0 ∨ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑌) ≠ 0 )))
108101, 107mpbird 246 . . . 4 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 )
10923adantr 480 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → (1r𝑅) ∈ 𝑆)
110109adantr 480 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (1r𝑅) ∈ 𝑆)
111 fvex 6113 . . . . . . . 8 (Base‘𝑅) ∈ V
11221, 111eqeltri 2684 . . . . . . 7 𝑆 ∈ V
1138, 112jctir 559 . . . . . 6 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (𝑋𝑌𝑆 ∈ V))
11438mapprop 41917 . . . . . 6 (((𝑋𝐵 ∧ (1r𝑅) ∈ 𝑆) ∧ (𝑌𝐵 ∧ ((invg𝑅)‘𝐴) ∈ 𝑆) ∧ (𝑋𝑌𝑆 ∈ V)) → {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ∈ (𝑆𝑚 {𝑋, 𝑌}))
11542, 110, 28, 34, 113, 114syl221anc 1329 . . . . 5 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ∈ (𝑆𝑚 {𝑋, 𝑌}))
116 breq1 4586 . . . . . . 7 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → (𝑓 finSupp 0 ↔ {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} finSupp 0 ))
117 oveq1 6556 . . . . . . . 8 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → (𝑓( linC ‘𝑀){𝑋, 𝑌}) = ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}))
118117eqeq1d 2612 . . . . . . 7 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → ((𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍))
119 fveq1 6102 . . . . . . . . 9 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → (𝑓𝑣) = ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣))
120119neeq1d 2841 . . . . . . . 8 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → ((𝑓𝑣) ≠ 0 ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ))
121120rexbidv 3034 . . . . . . 7 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → (∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 ↔ ∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ))
122116, 118, 1213anbi123d 1391 . . . . . 6 (𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 ) ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} finSupp 0 ∧ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 )))
123122adantl 481 . . . . 5 ((((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) ∧ 𝑓 = {⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 ) ↔ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} finSupp 0 ∧ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 )))
124115, 123rspcedv 3286 . . . 4 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → (({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} finSupp 0 ∧ ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({⟨𝑋, (1r𝑅)⟩, ⟨𝑌, ((invg𝑅)‘𝐴)⟩}‘𝑣) ≠ 0 ) → ∃𝑓 ∈ (𝑆𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 )))
12517, 50, 108, 124mp3and 1419 . . 3 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ∃𝑓 ∈ (𝑆𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 ))
126 prelpwi 4842 . . . . . 6 ((𝑋𝐵𝑌𝐵) → {𝑋, 𝑌} ∈ 𝒫 𝐵)
1271263adant3 1074 . . . . 5 ((𝑋𝐵𝑌𝐵𝑋𝑌) → {𝑋, 𝑌} ∈ 𝒫 𝐵)
128127ad2antlr 759 . . . 4 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} ∈ 𝒫 𝐵)
12935, 47, 20, 21, 13islindeps 42036 . . . 4 ((𝑀 ∈ LMod ∧ {𝑋, 𝑌} ∈ 𝒫 𝐵) → ({𝑋, 𝑌} linDepS 𝑀 ↔ ∃𝑓 ∈ (𝑆𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 )))
13041, 128, 129syl2anc 691 . . 3 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → ({𝑋, 𝑌} linDepS 𝑀 ↔ ∃𝑓 ∈ (𝑆𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓𝑣) ≠ 0 )))
131125, 130mpbird 246 . 2 (((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) ∧ (𝐴𝑆𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} linDepS 𝑀)
132131ex 449 1 ((𝑀 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑋𝑌)) → ((𝐴𝑆𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  Vcvv 3173  𝒫 cpw 4108  {csn 4125  {cpr 4127  ⟨cop 4131   class class class wbr 4583  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑𝑚 cmap 7744  Fincfn 7841   finSupp cfsupp 8158  Basecbs 15695  +gcplusg 15768  Scalarcsca 15771   ·𝑠 cvsca 15772  0gc0g 15923  Grpcgrp 17245  invgcminusg 17246  1rcur 18324  Ringcrg 18370  LModclmod 18686   linC clinc 41987   linDepS clindeps 42024 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-lmod 18688  df-linc 41989  df-lininds 42025  df-lindeps 42027 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator