Step | Hyp | Ref
| Expression |
1 | | qsdrng.q |
. . . 4
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀)) |
2 | | eqid 2732 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | qsdrng.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ NzRing) |
4 | | nzrring 20247 |
. . . . 5
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | | qsdrngi.1 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) |
7 | 2 | mxidlidl 32494 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) |
8 | 5, 6, 7 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) |
9 | | qsdrng.0 |
. . . . . . . . 9
⊢ 𝑂 =
(oppr‘𝑅) |
10 | 9 | opprring 20115 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) |
11 | 5, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ Ring) |
12 | | qsdrngi.2 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑂)) |
13 | | eqid 2732 |
. . . . . . . 8
⊢
(Base‘𝑂) =
(Base‘𝑂) |
14 | 13 | mxidlidl 32494 |
. . . . . . 7
⊢ ((𝑂 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑂)) → 𝑀 ∈ (LIdeal‘𝑂)) |
15 | 11, 12, 14 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑂)) |
16 | 8, 15 | elind 4191 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ((LIdeal‘𝑅) ∩ (LIdeal‘𝑂))) |
17 | | eqid 2732 |
. . . . . 6
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
18 | | eqid 2732 |
. . . . . 6
⊢
(LIdeal‘𝑂) =
(LIdeal‘𝑂) |
19 | | eqid 2732 |
. . . . . 6
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
20 | 17, 9, 18, 19 | 2idlval 20806 |
. . . . 5
⊢
(2Ideal‘𝑅) =
((LIdeal‘𝑅) ∩
(LIdeal‘𝑂)) |
21 | 16, 20 | eleqtrrdi 2844 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (2Ideal‘𝑅)) |
22 | 2 | mxidlnr 32495 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ (Base‘𝑅)) |
23 | 5, 6, 22 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ (Base‘𝑅)) |
24 | 1, 2, 5, 3, 21, 23 | qsnzr 32489 |
. . 3
⊢ (𝜑 → 𝑄 ∈ NzRing) |
25 | | eqid 2732 |
. . . 4
⊢
(1r‘𝑄) = (1r‘𝑄) |
26 | | eqid 2732 |
. . . 4
⊢
(0g‘𝑄) = (0g‘𝑄) |
27 | 25, 26 | nzrnz 20246 |
. . 3
⊢ (𝑄 ∈ NzRing →
(1r‘𝑄)
≠ (0g‘𝑄)) |
28 | 24, 27 | syl 17 |
. 2
⊢ (𝜑 → (1r‘𝑄) ≠
(0g‘𝑄)) |
29 | | eqid 2732 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑄) =
(Base‘𝑄) |
30 | | eqid 2732 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑄) = (.r‘𝑄) |
31 | | eqid 2732 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑄) =
(Unit‘𝑄) |
32 | 1, 19 | qusring 20811 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) |
33 | 5, 21, 32 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ∈ Ring) |
34 | 33 | ad10antr 742 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) → 𝑄 ∈ Ring) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑄 ∈ Ring) |
36 | | eldifi 4123 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})
→ 𝑢 ∈
(Base‘𝑄)) |
37 | 36 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → 𝑢 ∈ (Base‘𝑄)) |
38 | 37 | ad10antr 742 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑢 ∈ (Base‘𝑄)) |
39 | | ovex 7427 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ~QG 𝑀) ∈ V |
40 | 39 | ecelqsi 8752 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ (Base‘𝑅) → [𝑟](𝑅 ~QG 𝑀) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
41 | 40 | ad4antlr 731 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑟](𝑅 ~QG 𝑀) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
42 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑄 = (𝑅 /s (𝑅 ~QG 𝑀))) |
43 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) |
44 | | ovexd 7429 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑅 ~QG 𝑀) ∈ V) |
45 | 42, 43, 44, 3 | qusbas 17475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = (Base‘𝑄)) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = (Base‘𝑄)) |
47 | 46 | ad10antr 742 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = (Base‘𝑄)) |
48 | 41, 47 | eleqtrd 2835 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑟](𝑅 ~QG 𝑀) ∈ (Base‘𝑄)) |
49 | 39 | ecelqsi 8752 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ (Base‘𝑅) → [𝑠](𝑅 ~QG 𝑀) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
50 | 49 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑠](𝑅 ~QG 𝑀) ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
51 | 50, 47 | eleqtrd 2835 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑠](𝑅 ~QG 𝑀) ∈ (Base‘𝑄)) |
52 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑣 = [𝑟](𝑅 ~QG 𝑀)) |
53 | | simp-9r 792 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑢 = [𝑥](𝑅 ~QG 𝑀)) |
54 | 53 | eqcomd 2738 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑥](𝑅 ~QG 𝑀) = 𝑢) |
55 | 52, 54 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = ([𝑟](𝑅 ~QG 𝑀)(.r‘𝑄)𝑢)) |
56 | | simp-7r 788 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) |
57 | 55, 56 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → ([𝑟](𝑅 ~QG 𝑀)(.r‘𝑄)𝑢) = (1r‘𝑄)) |
58 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
⊢
(oppr‘𝑄) = (oppr‘𝑄) |
59 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘(oppr‘𝑄)) =
(.r‘(oppr‘𝑄)) |
60 | 29, 30, 58, 59 | opprmul 20107 |
. . . . . . . . . . . . . . 15
⊢ ([𝑠](𝑅 ~QG 𝑀)(.r‘(oppr‘𝑄))𝑢) = (𝑢(.r‘𝑄)[𝑠](𝑅
~QG 𝑀)) |
61 | | simp-5r 784 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
62 | 5 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑅 ∈ Ring) |
63 | 62 | ad8antr 738 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑅 ∈ Ring) |
64 | 21 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑀 ∈ (2Ideal‘𝑅)) |
65 | 64 | ad8antr 738 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑀 ∈ (2Ideal‘𝑅)) |
66 | 2, 9, 1, 63, 65, 29, 51, 38 | opprqusmulr 32515 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → ([𝑠](𝑅 ~QG 𝑀)(.r‘(oppr‘𝑄))𝑢) = ([𝑠](𝑅
~QG 𝑀)(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))𝑢)) |
67 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑤 = [𝑠](𝑅 ~QG 𝑀)) |
68 | 2, 17 | lidlss 20783 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ (LIdeal‘𝑅) → 𝑀 ⊆ (Base‘𝑅)) |
69 | 8, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ⊆ (Base‘𝑅)) |
70 | 9, 2 | oppreqg 32507 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ⊆ (Base‘𝑅)) → (𝑅 ~QG 𝑀) = (𝑂 ~QG 𝑀)) |
71 | 5, 69, 70 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑅 ~QG 𝑀) = (𝑂 ~QG 𝑀)) |
72 | 71 | ad10antr 742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) → (𝑅 ~QG 𝑀) = (𝑂 ~QG 𝑀)) |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑅 ~QG 𝑀) = (𝑂 ~QG 𝑀)) |
74 | 73 | eceq2d 8730 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑥](𝑅 ~QG 𝑀) = [𝑥](𝑂 ~QG 𝑀)) |
75 | 53, 74 | eqtr2d 2773 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑥](𝑂 ~QG 𝑀) = 𝑢) |
76 | 67, 75 | oveq12d 7412 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = ([𝑠](𝑅 ~QG 𝑀)(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))𝑢)) |
77 | 66, 76 | eqtr4d 2775 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → ([𝑠](𝑅 ~QG 𝑀)(.r‘(oppr‘𝑄))𝑢) = (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂
~QG 𝑀))) |
78 | 58, 25 | oppr1 20118 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1r‘𝑄) =
(1r‘(oppr‘𝑄)) |
79 | 2, 9, 1, 5, 21 | opprqus1r 32516 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(1r‘(oppr‘𝑄)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
80 | 78, 79 | eqtrid 2784 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1r‘𝑄) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
81 | 80 | ad10antr 742 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) → (1r‘𝑄) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (1r‘𝑄) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
83 | 61, 77, 82 | 3eqtr4d 2782 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → ([𝑠](𝑅 ~QG 𝑀)(.r‘(oppr‘𝑄))𝑢) = (1r‘𝑄)) |
84 | 60, 83 | eqtr3id 2786 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑢(.r‘𝑄)[𝑠](𝑅 ~QG 𝑀)) = (1r‘𝑄)) |
85 | 29, 26, 25, 30, 31, 35, 38, 48, 51, 57, 84 | ringinveu 32320 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → [𝑠](𝑅 ~QG 𝑀) = [𝑟](𝑅 ~QG 𝑀)) |
86 | 85, 67, 52 | 3eqtr4rd 2783 |
. . . . . . . . . . . 12
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → 𝑣 = 𝑤) |
87 | 86 | oveq2d 7410 |
. . . . . . . . . . 11
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑢(.r‘𝑄)𝑣) = (𝑢(.r‘𝑄)𝑤)) |
88 | 67 | oveq2d 7410 |
. . . . . . . . . . 11
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑢(.r‘𝑄)𝑤) = (𝑢(.r‘𝑄)[𝑠](𝑅 ~QG 𝑀))) |
89 | 87, 88, 84 | 3eqtrd 2776 |
. . . . . . . . . 10
⊢
((((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) ∧ 𝑠 ∈ (Base‘𝑅)) ∧ 𝑤 = [𝑠](𝑅 ~QG 𝑀)) → (𝑢(.r‘𝑄)𝑣) = (1r‘𝑄)) |
90 | | simp-4r 782 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
91 | 71 | qseq2d 8745 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = ((Base‘𝑅) / (𝑂 ~QG 𝑀))) |
92 | 91 | ad9antr 740 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = ((Base‘𝑅) / (𝑂 ~QG 𝑀))) |
93 | | eqidd 2733 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → (𝑂 /s (𝑂 ~QG 𝑀)) = (𝑂 /s (𝑂 ~QG 𝑀))) |
94 | 9, 2 | opprbas 20111 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅) =
(Base‘𝑂) |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → (Base‘𝑅) = (Base‘𝑂)) |
96 | | ovexd 7429 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → (𝑂 ~QG 𝑀) ∈ V) |
97 | 9 | fvexi 6893 |
. . . . . . . . . . . . . . 15
⊢ 𝑂 ∈ V |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → 𝑂 ∈ V) |
99 | 93, 95, 96, 98 | qusbas 17475 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → ((Base‘𝑅) / (𝑂 ~QG 𝑀)) = (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
100 | 92, 99 | eqtr2d 2773 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → (Base‘(𝑂 /s (𝑂 ~QG 𝑀))) = ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
101 | 90, 100 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → 𝑤 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
102 | | elqsi 8749 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀)) → ∃𝑠 ∈ (Base‘𝑅)𝑤 = [𝑠](𝑅 ~QG 𝑀)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → ∃𝑠 ∈ (Base‘𝑅)𝑤 = [𝑠](𝑅 ~QG 𝑀)) |
104 | 89, 103 | r19.29a 3162 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ 𝑟 ∈ (Base‘𝑅)) ∧ 𝑣 = [𝑟](𝑅 ~QG 𝑀)) → (𝑢(.r‘𝑄)𝑣) = (1r‘𝑄)) |
105 | | simp-4r 782 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) → 𝑣 ∈ (Base‘𝑄)) |
106 | 46 | ad6antr 734 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) → ((Base‘𝑅) / (𝑅 ~QG 𝑀)) = (Base‘𝑄)) |
107 | 105, 106 | eleqtrrd 2836 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) → 𝑣 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
108 | | elqsi 8749 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀)) → ∃𝑟 ∈ (Base‘𝑅)𝑣 = [𝑟](𝑅 ~QG 𝑀)) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) → ∃𝑟 ∈ (Base‘𝑅)𝑣 = [𝑟](𝑅 ~QG 𝑀)) |
110 | 104, 109 | r19.29a 3162 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) ∧ 𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))) ∧ (𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) → (𝑢(.r‘𝑄)𝑣) = (1r‘𝑄)) |
111 | | eqid 2732 |
. . . . . . . . . 10
⊢
(oppr‘𝑂) = (oppr‘𝑂) |
112 | | eqid 2732 |
. . . . . . . . . 10
⊢ (𝑂 /s (𝑂 ~QG 𝑀)) = (𝑂 /s (𝑂 ~QG 𝑀)) |
113 | 3 | ad3antrrr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑅 ∈ NzRing) |
114 | 9 | opprnzr 20251 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ NzRing → 𝑂 ∈ NzRing) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑂 ∈ NzRing) |
116 | 12 | ad3antrrr 728 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑀 ∈ (MaxIdeal‘𝑂)) |
117 | 6 | ad3antrrr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑀 ∈ (MaxIdeal‘𝑅)) |
118 | 9, 62, 117 | opprmxidlabs 32511 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑀 ∈
(MaxIdeal‘(oppr‘𝑂))) |
119 | | simplr 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑥 ∈ (Base‘𝑅)) |
120 | 94 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → (Base‘𝑅) = (Base‘𝑂)) |
121 | 119, 120 | eleqtrd 2835 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → 𝑥 ∈ (Base‘𝑂)) |
122 | | simplr 767 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → 𝑢 = [𝑥](𝑅 ~QG 𝑀)) |
123 | 5 | ringgrpd 20025 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ Grp) |
124 | 123 | ad4antr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → 𝑅 ∈ Grp) |
125 | | lidlnsg 32479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (LIdeal‘𝑅)) → 𝑀 ∈ (NrmSGrp‘𝑅)) |
126 | 5, 8, 125 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ (NrmSGrp‘𝑅)) |
127 | | nsgsubg 19012 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ (NrmSGrp‘𝑅) → 𝑀 ∈ (SubGrp‘𝑅)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ (SubGrp‘𝑅)) |
129 | 128 | ad4antr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → 𝑀 ∈ (SubGrp‘𝑅)) |
130 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → 𝑥 ∈ 𝑀) |
131 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ~QG 𝑀) = (𝑅 ~QG 𝑀) |
132 | 131 | eqg0el 32399 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Grp ∧ 𝑀 ∈ (SubGrp‘𝑅)) → ([𝑥](𝑅 ~QG 𝑀) = 𝑀 ↔ 𝑥 ∈ 𝑀)) |
133 | 132 | biimpar 478 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Grp ∧ 𝑀 ∈ (SubGrp‘𝑅)) ∧ 𝑥 ∈ 𝑀) → [𝑥](𝑅 ~QG 𝑀) = 𝑀) |
134 | 124, 129,
130, 133 | syl21anc 836 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → [𝑥](𝑅 ~QG 𝑀) = 𝑀) |
135 | | eqid 2732 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑅) = (0g‘𝑅) |
136 | 2, 131, 135 | eqgid 19034 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (SubGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝑀) = 𝑀) |
137 | 129, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → [(0g‘𝑅)](𝑅 ~QG 𝑀) = 𝑀) |
138 | 134, 137 | eqtr4d 2775 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → [𝑥](𝑅 ~QG 𝑀) = [(0g‘𝑅)](𝑅 ~QG 𝑀)) |
139 | 1, 135 | qus0 19040 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝑀) = (0g‘𝑄)) |
140 | 126, 139 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
[(0g‘𝑅)](𝑅 ~QG 𝑀) = (0g‘𝑄)) |
141 | 140 | ad4antr 730 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → [(0g‘𝑅)](𝑅 ~QG 𝑀) = (0g‘𝑄)) |
142 | 122, 138,
141 | 3eqtrd 2776 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → 𝑢 = (0g‘𝑄)) |
143 | | eldifsnneq 4788 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})
→ ¬ 𝑢 =
(0g‘𝑄)) |
144 | 143 | ad4antlr 731 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑥 ∈ 𝑀) → ¬ 𝑢 = (0g‘𝑄)) |
145 | 142, 144 | pm2.65da 815 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → ¬ 𝑥 ∈ 𝑀) |
146 | 111, 112,
115, 116, 118, 121, 145 | qsdrngilem 32518 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → ∃𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))(𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
147 | 146 | ad2antrr 724 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → ∃𝑤 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝑀)))(𝑤(.r‘(𝑂 /s (𝑂 ~QG 𝑀)))[𝑥](𝑂 ~QG 𝑀)) = (1r‘(𝑂 /s (𝑂 ~QG 𝑀)))) |
148 | 110, 147 | r19.29a 3162 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → (𝑢(.r‘𝑄)𝑣) = (1r‘𝑄)) |
149 | | simpllr 774 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → 𝑢 = [𝑥](𝑅 ~QG 𝑀)) |
150 | 149 | oveq2d 7410 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → (𝑣(.r‘𝑄)𝑢) = (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀))) |
151 | | simpr 485 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) |
152 | 150, 151 | eqtrd 2772 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄)) |
153 | 148, 152 | jca 512 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ 𝑣 ∈ (Base‘𝑄)) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) → ((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))) |
154 | 153 | anasss 467 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)}))
∧ 𝑥 ∈
(Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) ∧ (𝑣 ∈ (Base‘𝑄) ∧ (𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄))) → ((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))) |
155 | 9, 1, 113, 117, 116, 119, 145 | qsdrngilem 32518 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → ∃𝑣 ∈ (Base‘𝑄)(𝑣(.r‘𝑄)[𝑥](𝑅 ~QG 𝑀)) = (1r‘𝑄)) |
156 | 154, 155 | reximddv 3171 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑢 = [𝑥](𝑅 ~QG 𝑀)) → ∃𝑣 ∈ (Base‘𝑄)((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))) |
157 | 37, 46 | eleqtrrd 2836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → 𝑢 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀))) |
158 | | elqsi 8749 |
. . . . 5
⊢ (𝑢 ∈ ((Base‘𝑅) / (𝑅 ~QG 𝑀)) → ∃𝑥 ∈ (Base‘𝑅)𝑢 = [𝑥](𝑅 ~QG 𝑀)) |
159 | 157, 158 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → ∃𝑥 ∈ (Base‘𝑅)𝑢 = [𝑥](𝑅 ~QG 𝑀)) |
160 | 156, 159 | r19.29a 3162 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → ∃𝑣 ∈ (Base‘𝑄)((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))) |
161 | 160 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})∃𝑣 ∈ (Base‘𝑄)((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))) |
162 | 29, 26, 25, 30, 31, 33 | isdrng4 32321 |
. 2
⊢ (𝜑 → (𝑄 ∈ DivRing ↔
((1r‘𝑄)
≠ (0g‘𝑄) ∧ ∀𝑢 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})∃𝑣 ∈ (Base‘𝑄)((𝑢(.r‘𝑄)𝑣) = (1r‘𝑄) ∧ (𝑣(.r‘𝑄)𝑢) = (1r‘𝑄))))) |
163 | 28, 161, 162 | mpbir2and 711 |
1
⊢ (𝜑 → 𝑄 ∈ DivRing) |