Proof of Theorem rngqiprnglin
Step | Hyp | Ref
| Expression |
1 | | rngqiprngim.p |
. . . . 5
⊢ 𝑃 = (𝑄 ×s 𝐽) |
2 | | eqid 2731 |
. . . . 5
⊢
(Base‘𝑄) =
(Base‘𝑄) |
3 | | eqid 2731 |
. . . . 5
⊢
(Base‘𝐽) =
(Base‘𝐽) |
4 | | rngqiprngim.q |
. . . . . . 7
⊢ 𝑄 = (𝑅 /s ∼ ) |
5 | 4 | ovexi 7446 |
. . . . . 6
⊢ 𝑄 ∈ V |
6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑄 ∈ V) |
7 | | rng2idlring.u |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Ring) |
8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐽 ∈ Ring) |
9 | | rng2idlring.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Rng) |
10 | | simpl 482 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
11 | | rngqiprngim.g |
. . . . . . 7
⊢ ∼ =
(𝑅 ~QG
𝐼) |
12 | | rng2idlring.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
13 | 11, 4, 12, 2 | quseccl0 19104 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵) → [𝑎] ∼ ∈
(Base‘𝑄)) |
14 | 9, 10, 13 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [𝑎] ∼ ∈
(Base‘𝑄)) |
15 | | rng2idlring.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
16 | | rng2idlring.j |
. . . . . . 7
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
17 | | rng2idlring.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
18 | | rng2idlring.1 |
. . . . . . 7
⊢ 1 =
(1r‘𝐽) |
19 | 9, 15, 16, 7, 12, 17, 18 | rngqiprngghmlem1 21050 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( 1 · 𝑎) ∈ (Base‘𝐽)) |
20 | 10, 19 | sylan2 592 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 1 · 𝑎) ∈ (Base‘𝐽)) |
21 | | simpr 484 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
22 | 11, 4, 12, 2 | quseccl0 19104 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵) → [𝑏] ∼ ∈
(Base‘𝑄)) |
23 | 9, 21, 22 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [𝑏] ∼ ∈
(Base‘𝑄)) |
24 | 9, 15, 16, 7, 12, 17, 18 | rngqiprngghmlem1 21050 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ( 1 · 𝑏) ∈ (Base‘𝐽)) |
25 | 21, 24 | sylan2 592 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 1 · 𝑏) ∈ (Base‘𝐽)) |
26 | 9, 15, 16, 7, 12, 17, 18, 11, 4 | rngqiprnglinlem3 21056 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ([𝑎] ∼
(.r‘𝑄)[𝑏] ∼ ) ∈
(Base‘𝑄)) |
27 | | eqid 2731 |
. . . . . 6
⊢
(.r‘𝐽) = (.r‘𝐽) |
28 | 3, 27, 8, 20, 25 | ringcld 20155 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( 1 · 𝑎)(.r‘𝐽)( 1 · 𝑏)) ∈ (Base‘𝐽)) |
29 | | eqid 2731 |
. . . . 5
⊢
(.r‘𝑄) = (.r‘𝑄) |
30 | | eqid 2731 |
. . . . 5
⊢
(.r‘𝑃) = (.r‘𝑃) |
31 | 1, 2, 3, 6, 8, 14,
20, 23, 25, 26, 28, 29, 27, 30 | xpsmul 17528 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (〈[𝑎] ∼ , ( 1 · 𝑎)〉(.r‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉) = 〈([𝑎] ∼
(.r‘𝑄)[𝑏] ∼ ), (( 1 · 𝑎)(.r‘𝐽)( 1 · 𝑏))〉) |
32 | 9, 15, 16, 7, 12, 17, 18, 11, 4 | rngqiprnglinlem2 21055 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → [(𝑎 · 𝑏)] ∼ = ([𝑎] ∼
(.r‘𝑄)[𝑏] ∼ )) |
33 | 32 | eqcomd 2737 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ([𝑎] ∼
(.r‘𝑄)[𝑏] ∼ ) = [(𝑎 · 𝑏)] ∼ ) |
34 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐼 ∈ (2Ideal‘𝑅)) |
35 | 16, 17 | ressmulr 17259 |
. . . . . . . . 9
⊢ (𝐼 ∈ (2Ideal‘𝑅) → · =
(.r‘𝐽)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → · =
(.r‘𝐽)) |
37 | 36 | eqcomd 2737 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (.r‘𝐽) = · ) |
38 | 37 | oveqd 7429 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( 1 · 𝑎)(.r‘𝐽)( 1 · 𝑏)) = (( 1 · 𝑎) · ( 1 · 𝑏))) |
39 | 9, 15, 16, 7, 12, 17, 18 | rngqiprnglinlem1 21054 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( 1 · 𝑎) · ( 1 · 𝑏)) = ( 1 · (𝑎 · 𝑏))) |
40 | 38, 39 | eqtrd 2771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( 1 · 𝑎)(.r‘𝐽)( 1 · 𝑏)) = ( 1 · (𝑎 · 𝑏))) |
41 | 33, 40 | opeq12d 4881 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 〈([𝑎] ∼
(.r‘𝑄)[𝑏] ∼ ), (( 1 · 𝑎)(.r‘𝐽)( 1 · 𝑏))〉 = 〈[(𝑎 · 𝑏)] ∼ , ( 1 · (𝑎 · 𝑏))〉) |
42 | 31, 41 | eqtr2d 2772 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 〈[(𝑎 · 𝑏)] ∼ , ( 1 · (𝑎 · 𝑏))〉 = (〈[𝑎] ∼ , ( 1 · 𝑎)〉(.r‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉)) |
43 | 9 | anim1i 614 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑅 ∈ Rng ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) |
44 | | 3anass 1094 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ (𝑅 ∈ Rng ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) |
45 | 43, 44 | sylibr 233 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) |
46 | 12, 17 | rngcl 20062 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
48 | | rngqiprngim.c |
. . . . 5
⊢ 𝐶 = (Base‘𝑄) |
49 | | rngqiprngim.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) |
50 | 9, 15, 16, 7, 12, 17, 18, 11, 4, 48, 1, 49 | rngqiprngimfv 21061 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 · 𝑏) ∈ 𝐵) → (𝐹‘(𝑎 · 𝑏)) = 〈[(𝑎 · 𝑏)] ∼ , ( 1 · (𝑎 · 𝑏))〉) |
51 | 47, 50 | syldan 590 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎 · 𝑏)) = 〈[(𝑎 · 𝑏)] ∼ , ( 1 · (𝑎 · 𝑏))〉) |
52 | 9, 15, 16, 7, 12, 17, 18, 11, 4, 48, 1, 49 | rngqiprngimfv 21061 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
53 | 10, 52 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
54 | 9, 15, 16, 7, 12, 17, 18, 11, 4, 48, 1, 49 | rngqiprngimfv 21061 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) = 〈[𝑏] ∼ , ( 1 · 𝑏)〉) |
55 | 21, 54 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) = 〈[𝑏] ∼ , ( 1 · 𝑏)〉) |
56 | 53, 55 | oveq12d 7430 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎)(.r‘𝑃)(𝐹‘𝑏)) = (〈[𝑎] ∼ , ( 1 · 𝑎)〉(.r‘𝑃)〈[𝑏] ∼ , ( 1 · 𝑏)〉)) |
57 | 42, 51, 56 | 3eqtr4d 2781 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎 · 𝑏)) = ((𝐹‘𝑎)(.r‘𝑃)(𝐹‘𝑏))) |
58 | 57 | ralrimivva 3199 |
1
⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐹‘(𝑎 · 𝑏)) = ((𝐹‘𝑎)(.r‘𝑃)(𝐹‘𝑏))) |