Metamath Proof Explorer

Theorem ldepspr

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)

Ref Expression
Hypotheses snlindsntor.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
snlindsntor.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
snlindsntor.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
snlindsntor.0 ⊢ 0 = ( 0g ‘ 𝑅 )
snlindsntor.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
snlindsntor.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
Assertion ldepspr ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → { 𝑋 , 𝑌 } linDepS 𝑀 ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 snlindsntor.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 snlindsntor.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
4 snlindsntor.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 snlindsntor.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
6 snlindsntor.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
7 3simpa ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
8 7 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
9 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
10 fvex ⊢ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V
11 9 10 pm3.2i ⊢ ( ( 1r ‘ 𝑅 ) ∈ V ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V )
12 11 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( 1r ‘ 𝑅 ) ∈ V ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V ) )
13 simp3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
14 13 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝑋 ≠ 𝑌 )
15 fprg ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 1r ‘ 𝑅 ) ∈ V ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V ) ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ { ( 1r ‘ 𝑅 ) , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) } )
16 8 12 14 15 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } : { 𝑋 , 𝑌 } ⟶ { ( 1r ‘ 𝑅 ) , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) } )
17 prfi ⊢ { 𝑋 , 𝑌 } ∈ Fin
18 17 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { 𝑋 , 𝑌 } ∈ Fin )
19 4 fvexi ⊢ 0 ∈ V
20 19 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 0 ∈ V )
21 16 18 20 fdmfifsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } finSupp 0 )
22 13 anim2i ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌 ) )
23 22 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌 ) )
24 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
25 2 3 24 lmod1cl ⊢ ( 𝑀 ∈ LMod → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
26 simp1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐵 )
27 25 26 anim12ci ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) )
28 27 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) )
29 simp2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐵 )
30 29 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝑌 ∈ 𝐵 )
31 2 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
32 31 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑅 ∈ Grp )
33 simpl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → 𝐴 ∈ 𝑆 )
34 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
35 3 34 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆 ) → ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ 𝑆 )
36 32 33 35 syl2an ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ 𝑆 )
37 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
38 eqid ⊢ { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ }
39 1 2 3 6 37 38 lincvalpr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ 𝑆 ) ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) · 𝑌 ) ) )
40 23 28 30 36 39 syl112anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) · 𝑌 ) ) )
41 simpll ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝑀 ∈ LMod )
42 26 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
43 33 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝐴 ∈ 𝑆 )
44 42 30 43 3jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) )
45 41 44 jca ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) )
46 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → 𝑋 = ( 𝐴 · 𝑌 ) )
47 1 2 3 4 5 6 24 34 ldepsprlem ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆 ) ) → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 ) )
48 45 46 47 sylc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( ( 1r ‘ 𝑅 ) · 𝑋 ) ( +g ‘ 𝑀 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) · 𝑌 ) ) = 𝑍 )
49 40 48 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 )
50 2 lmodring ⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
51 eqcom ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ↔ ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
52 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
53 3 52 24 01eq0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) ) → 𝑆 = { ( 0g ‘ 𝑅 ) } )
54 sneq ⊢ ( ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) → { ( 0g ‘ 𝑅 ) } = { ( 1r ‘ 𝑅 ) } )
55 54 eqeq2d ⊢ ( ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) → ( 𝑆 = { ( 0g ‘ 𝑅 ) } ↔ 𝑆 = { ( 1r ‘ 𝑅 ) } ) )
56 eleq2 ⊢ ( 𝑆 = { ( 1r ‘ 𝑅 ) } → ( 𝐴 ∈ 𝑆 ↔ 𝐴 ∈ { ( 1r ‘ 𝑅 ) } ) )
57 elsni ⊢ ( 𝐴 ∈ { ( 1r ‘ 𝑅 ) } → 𝐴 = ( 1r ‘ 𝑅 ) )
58 oveq1 ⊢ ( 𝐴 = ( 1r ‘ 𝑅 ) → ( 𝐴 · 𝑌 ) = ( ( 1r ‘ 𝑅 ) · 𝑌 ) )
59 58 eqeq2d ⊢ ( 𝐴 = ( 1r ‘ 𝑅 ) → ( 𝑋 = ( 𝐴 · 𝑌 ) ↔ 𝑋 = ( ( 1r ‘ 𝑅 ) · 𝑌 ) ) )
60 29 anim1i ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( 𝑌 ∈ 𝐵 ∧ 𝑀 ∈ LMod ) )
61 60 ancomd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) )
62 1 2 6 24 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
63 61 62 syl ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( ( 1r ‘ 𝑅 ) · 𝑌 ) = 𝑌 )
64 63 eqeq2d ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( 𝑋 = ( ( 1r ‘ 𝑅 ) · 𝑌 ) ↔ 𝑋 = 𝑌 ) )
65 eqneqall ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≠ 𝑌 → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
66 65 com12 ⊢ ( 𝑋 ≠ 𝑌 → ( 𝑋 = 𝑌 → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
67 66 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 = 𝑌 → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
68 67 adantr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( 𝑋 = 𝑌 → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
69 64 68 sylbid ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑀 ∈ LMod ) → ( 𝑋 = ( ( 1r ‘ 𝑅 ) · 𝑌 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
70 69 ex ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( 𝑋 = ( ( 1r ‘ 𝑅 ) · 𝑌 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) )
71 70 com3r ⊢ ( 𝑋 = ( ( 1r ‘ 𝑅 ) · 𝑌 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) )
72 59 71 biimtrdi ⊢ ( 𝐴 = ( 1r ‘ 𝑅 ) → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
73 57 72 syl ⊢ ( 𝐴 ∈ { ( 1r ‘ 𝑅 ) } → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
74 56 73 biimtrdi ⊢ ( 𝑆 = { ( 1r ‘ 𝑅 ) } → ( 𝐴 ∈ 𝑆 → ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
75 74 impd ⊢ ( 𝑆 = { ( 1r ‘ 𝑅 ) } → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
76 75 com23 ⊢ ( 𝑆 = { ( 1r ‘ 𝑅 ) } → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
77 55 76 biimtrdi ⊢ ( ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) → ( 𝑆 = { ( 0g ‘ 𝑅 ) } → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
78 77 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑆 = { ( 0g ‘ 𝑅 ) } → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
79 53 78 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
80 79 ex ⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
81 51 80 biimtrid ⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( 𝑀 ∈ LMod → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
82 81 com25 ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ LMod → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) ) )
83 50 82 mpcom ⊢ ( 𝑀 ∈ LMod → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) ) ) )
84 83 imp31 ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
85 orc ⊢ ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) )
86 84 85 pm2.61d1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) )
87 4 eqeq2i ⊢ ( ( 1r ‘ 𝑅 ) = 0 ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
88 87 necon3abii ⊢ ( ( 1r ‘ 𝑅 ) ≠ 0 ↔ ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
89 88 orbi1i ⊢ ( ( ( 1r ‘ 𝑅 ) ≠ 0 ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ↔ ( ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) )
90 86 89 sylibr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( 1r ‘ 𝑅 ) ≠ 0 ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) )
91 fvexd ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 1r ‘ 𝑅 ) ∈ V )
92 fvpr1g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ V ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) = ( 1r ‘ 𝑅 ) )
93 42 91 14 92 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) = ( 1r ‘ 𝑅 ) )
94 93 neeq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
95 fvexd ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V )
96 fvpr2g ⊢ ( ( 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ V ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) = ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) )
97 30 95 14 96 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) = ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) )
98 97 neeq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ↔ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) )
99 94 98 orbi12d ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ∨ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ) ↔ ( ( 1r ‘ 𝑅 ) ≠ 0 ∨ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ≠ 0 ) ) )
100 90 99 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ∨ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ) )
101 fveq2 ⊢ ( 𝑣 = 𝑋 → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) = ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) )
102 101 neeq1d ⊢ ( 𝑣 = 𝑋 → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ) )
103 fveq2 ⊢ ( 𝑣 = 𝑌 → ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) = ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) )
104 103 neeq1d ⊢ ( 𝑣 = 𝑌 → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ) )
105 102 104 rexprg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ↔ ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ∨ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ) ) )
106 8 105 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ↔ ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑋 ) ≠ 0 ∨ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑌 ) ≠ 0 ) ) )
107 100 106 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 )
108 25 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
109 108 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
110 3 fvexi ⊢ 𝑆 ∈ V
111 14 110 jctir ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( 𝑋 ≠ 𝑌 ∧ 𝑆 ∈ V ) )
112 38 mapprop ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ∈ 𝑆 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑆 ∈ V ) ) → { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) )
113 42 109 30 36 111 112 syl221anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) )
114 breq1 ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( 𝑓 finSupp 0 ↔ { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } finSupp 0 ) )
115 oveq1 ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) )
116 115 eqeq1d ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ) )
117 fveq1 ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( 𝑓 ‘ 𝑣 ) = ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) )
118 117 neeq1d ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( ( 𝑓 ‘ 𝑣 ) ≠ 0 ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ) )
119 118 rexbidv ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ↔ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ) )
120 114 116 119 3anbi123d ⊢ ( 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } finSupp 0 ∧ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ) ) )
121 120 adantl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) ∧ 𝑓 = { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) ↔ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } finSupp 0 ∧ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ) ) )
122 113 121 rspcedv ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } finSupp 0 ∧ ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( { ⟨ 𝑋 , ( 1r ‘ 𝑅 ) ⟩ , ⟨ 𝑌 , ( ( invg ‘ 𝑅 ) ‘ 𝐴 ) ⟩ } ‘ 𝑣 ) ≠ 0 ) → ∃ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) ) )
123 21 49 107 122 mp3and ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ∃ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) )
124 prelpwi ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → { 𝑋 , 𝑌 } ∈ 𝒫 𝐵 )
125 124 3adant3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝒫 𝐵 )
126 125 ad2antlr ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { 𝑋 , 𝑌 } ∈ 𝒫 𝐵 )
127 1 5 2 3 4 islindeps ⊢ ( ( 𝑀 ∈ LMod ∧ { 𝑋 , 𝑌 } ∈ 𝒫 𝐵 ) → ( { 𝑋 , 𝑌 } linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) ) )
128 41 126 127 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → ( { 𝑋 , 𝑌 } linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 , 𝑌 } ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 , 𝑌 } ) = 𝑍 ∧ ∃ 𝑣 ∈ { 𝑋 , 𝑌 } ( 𝑓 ‘ 𝑣 ) ≠ 0 ) ) )
129 123 128 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) ) → { 𝑋 , 𝑌 } linDepS 𝑀 )
130 129 ex ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 = ( 𝐴 · 𝑌 ) ) → { 𝑋 , 𝑌 } linDepS 𝑀 ) )