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

Metamath Proof Explorer

Theorem lspsolvlem

Description: Lemma for lspsolv . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lspsolv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsolv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspsolv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsolv.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lspsolv.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
lspsolv.p ⊢ + = ( +g ‘ 𝑊 )
lspsolv.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsolv.q ⊢ 𝑄 = { 𝑧 ∈ 𝑉 ∣ ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) }
lspsolv.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsolv.ss ⊢ ( 𝜑 → 𝐴 ⊆ 𝑉 )
lspsolv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspsolv.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) )
Assertion lspsolvlem ( 𝜑 → ∃ 𝑟 ∈ 𝐵 ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 lspsolv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsolv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspsolv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsolv.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5 lspsolv.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
6 lspsolv.p ⊢ + = ( +g ‘ 𝑊 )
7 lspsolv.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
8 lspsolv.q ⊢ 𝑄 = { 𝑧 ∈ 𝑉 ∣ ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) }
9 lspsolv.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
10 lspsolv.ss ⊢ ( 𝜑 → 𝐴 ⊆ 𝑉 )
11 lspsolv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12 lspsolv.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) )
13 8 ssrab3 ⊢ 𝑄 ⊆ 𝑉
14 13 a1i ⊢ ( 𝜑 → 𝑄 ⊆ 𝑉 )
15 9 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑊 ∈ LMod )
16 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
17 4 5 16 lmod0cl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝐹 ) ∈ 𝐵 )
18 15 17 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 0g ‘ 𝐹 ) ∈ 𝐵 )
19 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
20 1 4 7 16 19 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑌 ) = ( 0g ‘ 𝑊 ) )
21 9 11 20 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝐹 ) · 𝑌 ) = ( 0g ‘ 𝑊 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 0g ‘ 𝐹 ) · 𝑌 ) = ( 0g ‘ 𝑊 ) )
23 22 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) = ( 𝑧 + ( 0g ‘ 𝑊 ) ) )
24 10 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝑉 )
25 1 6 19 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉 ) → ( 𝑧 + ( 0g ‘ 𝑊 ) ) = 𝑧 )
26 15 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 + ( 0g ‘ 𝑊 ) ) = 𝑧 )
27 23 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) = 𝑧 )
28 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉 ) → 𝐴 ⊆ ( 𝑁 ‘ 𝐴 ) )
29 9 10 28 syl2anc ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑁 ‘ 𝐴 ) )
30 29 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝑁 ‘ 𝐴 ) )
31 27 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
32 oveq1 ⊢ ( 𝑟 = ( 0g ‘ 𝐹 ) → ( 𝑟 · 𝑌 ) = ( ( 0g ‘ 𝐹 ) · 𝑌 ) )
33 32 oveq2d ⊢ ( 𝑟 = ( 0g ‘ 𝐹 ) → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) )
34 33 eleq1d ⊢ ( 𝑟 = ( 0g ‘ 𝐹 ) → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
35 34 rspcev ⊢ ( ( ( 0g ‘ 𝐹 ) ∈ 𝐵 ∧ ( 𝑧 + ( ( 0g ‘ 𝐹 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
36 18 31 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
37 10 36 ssrabdv ⊢ ( 𝜑 → 𝐴 ⊆ { 𝑧 ∈ 𝑉 ∣ ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) } )
38 37 8 sseqtrrdi ⊢ ( 𝜑 → 𝐴 ⊆ 𝑄 )
39 4 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
40 9 39 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
41 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
42 4 5 41 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝐹 ) ∈ 𝐵 )
43 9 42 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐵 )
44 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
45 5 44 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ ( 1r ‘ 𝐹 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐵 )
46 40 43 45 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐵 )
47 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
48 1 47 4 7 41 44 lmodvneg1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) = ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) )
49 9 11 48 syl2anc ⊢ ( 𝜑 → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) = ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) )
50 49 oveq2d ⊢ ( 𝜑 → ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) = ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) )
51 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
52 9 51 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
53 1 6 19 47 grprinv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) = ( 0g ‘ 𝑊 ) )
54 52 11 53 syl2anc ⊢ ( 𝜑 → ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) = ( 0g ‘ 𝑊 ) )
55 50 54 eqtrd ⊢ ( 𝜑 → ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) = ( 0g ‘ 𝑊 ) )
56 1 2 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 )
57 9 10 56 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 )
58 19 2 lss0cl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ ( 𝑁 ‘ 𝐴 ) )
59 9 57 58 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ ( 𝑁 ‘ 𝐴 ) )
60 55 59 eqeltrd ⊢ ( 𝜑 → ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
61 oveq1 ⊢ ( 𝑟 = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) → ( 𝑟 · 𝑌 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) )
62 61 oveq2d ⊢ ( 𝑟 = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) → ( 𝑌 + ( 𝑟 · 𝑌 ) ) = ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) )
63 62 eleq1d ⊢ ( 𝑟 = ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) → ( ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
64 63 rspcev ⊢ ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑌 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
65 46 60 64 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝐵 ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
66 oveq1 ⊢ ( 𝑧 = 𝑌 → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( 𝑌 + ( 𝑟 · 𝑌 ) ) )
67 66 eleq1d ⊢ ( 𝑧 = 𝑌 → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
68 67 rexbidv ⊢ ( 𝑧 = 𝑌 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
69 68 8 elrab2 ⊢ ( 𝑌 ∈ 𝑄 ↔ ( 𝑌 ∈ 𝑉 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑌 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
70 11 65 69 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ 𝑄 )
71 70 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑄 )
72 38 71 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑌 } ) ⊆ 𝑄 )
73 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ⊆ 𝑉 ∧ ( 𝐴 ∪ { 𝑌 } ) ⊆ 𝑄 ) → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ⊆ ( 𝑁 ‘ 𝑄 ) )
74 9 14 72 73 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ⊆ ( 𝑁 ‘ 𝑄 ) )
75 4 a1i ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
76 5 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐹 ) )
77 1 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
78 6 a1i ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
79 7 a1i ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
80 2 a1i ⊢ ( 𝜑 → 𝑆 = ( LSubSp ‘ 𝑊 ) )
81 70 ne0d ⊢ ( 𝜑 → 𝑄 ≠ ∅ )
82 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( 𝑥 + ( 𝑟 · 𝑌 ) ) )
83 82 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑥 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
84 83 rexbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
85 oveq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 · 𝑌 ) = ( 𝑠 · 𝑌 ) )
86 85 oveq2d ⊢ ( 𝑟 = 𝑠 → ( 𝑥 + ( 𝑟 · 𝑌 ) ) = ( 𝑥 + ( 𝑠 · 𝑌 ) ) )
87 86 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑥 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
88 87 cbvrexvw ⊢ ( ∃ 𝑟 ∈ 𝐵 ( 𝑥 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
89 84 88 bitrdi ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
90 89 8 elrab2 ⊢ ( 𝑥 ∈ 𝑄 ↔ ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
91 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( 𝑦 + ( 𝑟 · 𝑌 ) ) )
92 91 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑦 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
93 92 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑦 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
94 oveq1 ⊢ ( 𝑟 = 𝑡 → ( 𝑟 · 𝑌 ) = ( 𝑡 · 𝑌 ) )
95 94 oveq2d ⊢ ( 𝑟 = 𝑡 → ( 𝑦 + ( 𝑟 · 𝑌 ) ) = ( 𝑦 + ( 𝑡 · 𝑌 ) ) )
96 95 eleq1d ⊢ ( 𝑟 = 𝑡 → ( ( 𝑦 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
97 96 cbvrexvw ⊢ ( ∃ 𝑟 ∈ 𝐵 ( 𝑦 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
98 93 97 bitrdi ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
99 98 8 elrab2 ⊢ ( 𝑦 ∈ 𝑄 ↔ ( 𝑦 ∈ 𝑉 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
100 90 99 anbi12i ⊢ ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄 ) ↔ ( ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝑉 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) )
101 an4 ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝑉 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) ↔ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) )
102 100 101 bitri ⊢ ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄 ) ↔ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) )
103 reeanv ⊢ ( ∃ 𝑠 ∈ 𝐵 ∃ 𝑡 ∈ 𝐵 ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ↔ ( ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
104 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝜑 )
105 104 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑊 ∈ LMod )
106 simp1lr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑎 ∈ 𝐵 )
107 simp1rl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑥 ∈ 𝑉 )
108 1 4 7 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑎 · 𝑥 ) ∈ 𝑉 )
109 105 106 107 108 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑎 · 𝑥 ) ∈ 𝑉 )
110 simp1rr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑦 ∈ 𝑉 )
111 1 6 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑥 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑉 )
112 105 109 110 111 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑉 )
113 simp2l ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑠 ∈ 𝐵 )
114 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
115 4 5 114 lmodmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ∈ 𝐵 )
116 105 106 113 115 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ∈ 𝐵 )
117 simp2r ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑡 ∈ 𝐵 )
118 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
119 4 5 118 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) ∈ 𝐵 )
120 105 116 117 119 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) ∈ 𝐵 )
121 104 11 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑌 ∈ 𝑉 )
122 1 4 7 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑠 · 𝑌 ) ∈ 𝑉 )
123 105 113 121 122 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑠 · 𝑌 ) ∈ 𝑉 )
124 1 4 7 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑠 · 𝑌 ) ∈ 𝑉 ) → ( 𝑎 · ( 𝑠 · 𝑌 ) ) ∈ 𝑉 )
125 105 106 123 124 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑎 · ( 𝑠 · 𝑌 ) ) ∈ 𝑉 )
126 1 4 7 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑡 · 𝑌 ) ∈ 𝑉 )
127 105 117 121 126 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑡 · 𝑌 ) ∈ 𝑉 )
128 1 6 lmod4 ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑎 · 𝑥 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) ∈ 𝑉 ∧ ( 𝑡 · 𝑌 ) ∈ 𝑉 ) ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) + ( 𝑡 · 𝑌 ) ) ) = ( ( ( 𝑎 · 𝑥 ) + ( 𝑎 · ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) )
129 105 109 110 125 127 128 syl122anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) + ( 𝑡 · 𝑌 ) ) ) = ( ( ( 𝑎 · 𝑥 ) + ( 𝑎 · ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) )
130 1 6 4 7 5 118 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) = ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) · 𝑌 ) + ( 𝑡 · 𝑌 ) ) )
131 105 116 117 121 130 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) = ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) · 𝑌 ) + ( 𝑡 · 𝑌 ) ) )
132 1 4 7 5 114 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) · 𝑌 ) = ( 𝑎 · ( 𝑠 · 𝑌 ) ) )
133 105 106 113 121 132 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) · 𝑌 ) = ( 𝑎 · ( 𝑠 · 𝑌 ) ) )
134 133 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) · 𝑌 ) + ( 𝑡 · 𝑌 ) ) = ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) + ( 𝑡 · 𝑌 ) ) )
135 131 134 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) = ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) + ( 𝑡 · 𝑌 ) ) )
136 135 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) = ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( 𝑎 · ( 𝑠 · 𝑌 ) ) + ( 𝑡 · 𝑌 ) ) ) )
137 1 6 4 7 5 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑠 · 𝑌 ) ∈ 𝑉 ) ) → ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) = ( ( 𝑎 · 𝑥 ) + ( 𝑎 · ( 𝑠 · 𝑌 ) ) ) )
138 105 106 107 123 137 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) = ( ( 𝑎 · 𝑥 ) + ( 𝑎 · ( 𝑠 · 𝑌 ) ) ) )
139 138 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) = ( ( ( 𝑎 · 𝑥 ) + ( 𝑎 · ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) )
140 129 136 139 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) = ( ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) )
141 104 57 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 )
142 simp3l ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
143 simp3r ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
144 4 5 6 7 2 lsscl ⊢ ( ( ( 𝑁 ‘ 𝐴 ) ∈ 𝑆 ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
145 141 106 142 143 144 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · ( 𝑥 + ( 𝑠 · 𝑌 ) ) ) + ( 𝑦 + ( 𝑡 · 𝑌 ) ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
146 140 145 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
147 oveq1 ⊢ ( 𝑟 = ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) → ( 𝑟 · 𝑌 ) = ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) )
148 147 oveq2d ⊢ ( 𝑟 = ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) → ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) = ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) )
149 148 eleq1d ⊢ ( 𝑟 = ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) → ( ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
150 149 rspcev ⊢ ( ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) ∈ 𝐵 ∧ ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( ( ( 𝑎 ( .r ‘ 𝐹 ) 𝑠 ) ( +g ‘ 𝐹 ) 𝑡 ) · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
151 120 146 150 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ∃ 𝑟 ∈ 𝐵 ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
152 oveq1 ⊢ ( 𝑧 = ( ( 𝑎 · 𝑥 ) + 𝑦 ) → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) )
153 152 eleq1d ⊢ ( 𝑧 = ( ( 𝑎 · 𝑥 ) + 𝑦 ) → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
154 153 rexbidv ⊢ ( 𝑧 = ( ( 𝑎 · 𝑥 ) + 𝑦 ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
155 154 8 elrab2 ⊢ ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ↔ ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑉 ∧ ∃ 𝑟 ∈ 𝐵 ( ( ( 𝑎 · 𝑥 ) + 𝑦 ) + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
156 112 151 155 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 )
157 156 3exp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) ) )
158 157 rexlimdvv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑠 ∈ 𝐵 ∃ 𝑡 ∈ 𝐵 ( ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) )
159 103 158 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) )
160 159 expimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ∃ 𝑠 ∈ 𝐵 ( 𝑥 + ( 𝑠 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑦 + ( 𝑡 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) )
161 102 160 biimtrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄 ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) )
162 161 exp4b ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝑥 ∈ 𝑄 → ( 𝑦 ∈ 𝑄 → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 ) ) ) )
163 162 3imp2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄 ) ) → ( ( 𝑎 · 𝑥 ) + 𝑦 ) ∈ 𝑄 )
164 75 76 77 78 79 80 14 81 163 islssd ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
165 2 3 lspid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆 ) → ( 𝑁 ‘ 𝑄 ) = 𝑄 )
166 9 164 165 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑄 ) = 𝑄 )
167 74 166 sseqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ⊆ 𝑄 )
168 167 12 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝑄 )
169 oveq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 + ( 𝑟 · 𝑌 ) ) = ( 𝑋 + ( 𝑟 · 𝑌 ) ) )
170 169 eleq1d ⊢ ( 𝑧 = 𝑋 → ( ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
171 170 rexbidv ⊢ ( 𝑧 = 𝑋 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑧 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
172 171 8 elrab2 ⊢ ( 𝑋 ∈ 𝑄 ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
173 172 simprbi ⊢ ( 𝑋 ∈ 𝑄 → ∃ 𝑟 ∈ 𝐵 ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
174 168 173 syl ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝐵 ( 𝑋 + ( 𝑟 · 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )