Step | Hyp | Ref
| Expression |
1 | | rng2idlring.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Rng) |
2 | | rng2idlring.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
3 | | rng2idlring.j |
. . 3
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
4 | | rng2idlring.u |
. . 3
⊢ (𝜑 → 𝐽 ∈ Ring) |
5 | | rng2idlring.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
6 | | rng2idlring.t |
. . 3
⊢ · =
(.r‘𝑅) |
7 | | rng2idlring.1 |
. . 3
⊢ 1 =
(1r‘𝐽) |
8 | | rngqiprngim.g |
. . 3
⊢ ∼ =
(𝑅 ~QG
𝐼) |
9 | | rngqiprngim.q |
. . 3
⊢ 𝑄 = (𝑅 /s ∼ ) |
10 | | rngqiprngim.c |
. . 3
⊢ 𝐶 = (Base‘𝑄) |
11 | | rngqiprngim.p |
. . 3
⊢ 𝑃 = (𝑄 ×s 𝐽) |
12 | | rngqiprngim.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | rngqiprngimf 21060 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼)) |
14 | | elxpi 5698 |
. . . . 5
⊢ (𝑏 ∈ (𝐶 × 𝐼) → ∃𝑝∃𝑞(𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼))) |
15 | 10 | eleq2i 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐶 ↔ 𝑝 ∈ (Base‘𝑄)) |
16 | | vex 3477 |
. . . . . . . . . . . . . . 15
⊢ 𝑝 ∈ V |
17 | 8, 9, 5 | quselbas 19103 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Rng ∧ 𝑝 ∈ V) → (𝑝 ∈ (Base‘𝑄) ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) |
18 | 1, 16, 17 | sylancl 585 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) |
19 | 15, 18 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑝 ∈ 𝐶 ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) |
20 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
⊢
(+g‘𝑅) = (+g‘𝑅) |
21 | | rnggrp 20056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
22 | 1, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ Grp) |
23 | 22 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Grp) |
24 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
25 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Rng) |
26 | 1, 2, 3, 4, 5, 6, 7 | rngqiprng1elbas 21049 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈ 𝐵) |
27 | 26 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 1 ∈ 𝐵) |
28 | 5, 6 | rngcl 20062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐵) |
29 | 25, 27, 24, 28 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐵) |
30 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(-g‘𝑅) = (-g‘𝑅) |
31 | 5, 30 | grpsubcl 18943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Grp ∧ 𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐) ∈ 𝐵) → (𝑐(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐵) |
32 | 23, 24, 29, 31 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑐(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐵) |
33 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
34 | 5, 33 | 2idlss 21021 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (2Ideal‘𝑅) → 𝐼 ⊆ 𝐵) |
35 | 2, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
36 | 35 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → 𝑞 ∈ 𝐵) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ 𝐵) |
38 | 5, 20, 23, 32, 37 | grpcld 18872 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) → ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵) |
40 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = [𝑐] ∼ → 〈𝑝, 𝑞〉 = 〈[𝑐] ∼ , 𝑞〉) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
〈𝑝, 𝑞〉 = 〈[𝑐] ∼ , 𝑞〉) |
42 | | eceq1 8747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → [𝑎] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ) |
43 | | oveq2 7420 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → ( 1 · 𝑎) = ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))) |
44 | 42, 43 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → 〈[𝑎] ∼ , ( 1 · 𝑎)〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) |
45 | 41, 44 | eqeqan12d 2745 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) ∧ 𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) → (〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ↔ 〈[𝑐] ∼ , 𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉)) |
46 | | rngabl 20053 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) |
47 | 1, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ∈ Abel) |
48 | 47 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Abel) |
49 | 5, 20, 30 | ablsubaddsub 19727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Abel ∧ (𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐) ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) = (𝑞(-g‘𝑅)( 1 · 𝑐))) |
50 | 48, 24, 29, 37, 49 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) = (𝑞(-g‘𝑅)( 1 · 𝑐))) |
51 | 4 | ringgrpd 20140 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐽 ∈ Grp) |
52 | 51 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐽 ∈ Grp) |
53 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘𝐽) =
(Base‘𝐽) |
54 | 2, 3, 53 | 2idlbas 21022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
55 | 54 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐼 = (Base‘𝐽)) |
56 | 55 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑞 ∈ 𝐼 ↔ 𝑞 ∈ (Base‘𝐽))) |
57 | 56 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → 𝑞 ∈ (Base‘𝐽)) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ (Base‘𝐽)) |
59 | 1, 2, 3, 4, 5, 6, 7 | rngqiprngghmlem1 21050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ (Base‘𝐽)) |
60 | 59 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ (Base‘𝐽)) |
61 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(-g‘𝐽) = (-g‘𝐽) |
62 | 53, 61 | grpsubcl 18943 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ Grp ∧ 𝑞 ∈ (Base‘𝐽) ∧ ( 1 · 𝑐) ∈ (Base‘𝐽)) → (𝑞(-g‘𝐽)( 1 · 𝑐)) ∈ (Base‘𝐽)) |
63 | 52, 58, 60, 62 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝐽)( 1 · 𝑐)) ∈ (Base‘𝐽)) |
64 | | ringrng 20177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) |
65 | 4, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐽 ∈ Rng) |
66 | 3, 65 | eqeltrrid 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) |
67 | 1, 2, 66 | rng2idlnsg 21043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
68 | | nsgsubg 19078 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) |
70 | 69 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐼 ∈ (SubGrp‘𝑅)) |
71 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ 𝐼) |
72 | 54 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (Base‘𝐽) = 𝐼) |
73 | 60, 72 | eleqtrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐼) |
74 | 30, 3, 61 | subgsub 19058 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ (SubGrp‘𝑅) ∧ 𝑞 ∈ 𝐼 ∧ ( 1 · 𝑐) ∈ 𝐼) → (𝑞(-g‘𝑅)( 1 · 𝑐)) = (𝑞(-g‘𝐽)( 1 · 𝑐))) |
75 | 70, 71, 73, 74 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝑅)( 1 · 𝑐)) = (𝑞(-g‘𝐽)( 1 · 𝑐))) |
76 | 55 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐼 = (Base‘𝐽)) |
77 | 63, 75, 76 | 3eltr4d 2847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐼) |
78 | 50, 77 | eqeltrd 2832 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼) |
79 | 5, 30, 8 | qusecsub 19748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Abel ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ (𝑐 ∈ 𝐵 ∧ ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵)) → ([𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ↔ (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼)) |
80 | 48, 70, 24, 38, 79 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ([𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ↔ (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼)) |
81 | 78, 80 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → [𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ) |
82 | 1, 2, 3, 4, 5, 6, 7 | rngqiprngimfolem 21053 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼 ∧ 𝑐 ∈ 𝐵) → ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) = 𝑞) |
83 | 82 | 3expa 1117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) = 𝑞) |
84 | 83 | eqcomd 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 = ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))) |
85 | 81, 84 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 〈[𝑐] ∼ , 𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
〈[𝑐] ∼ ,
𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) |
87 | 39, 45, 86 | rspcedvd 3614 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
88 | 87 | rexlimdva2 3156 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
89 | 88 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑞 ∈ 𝐼 → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) |
90 | 89 | com23 86 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → (𝑞 ∈ 𝐼 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) |
91 | 19, 90 | sylbid 239 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑝 ∈ 𝐶 → (𝑞 ∈ 𝐼 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) |
92 | 91 | impd 410 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼) → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
93 | 92 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼) → (𝜑 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
94 | 93 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
95 | 94 | imp 406 |
. . . . . . . 8
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
96 | | simplll 772 |
. . . . . . . . . 10
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → 𝑏 = 〈𝑝, 𝑞〉) |
97 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | rngqiprngimfv 21061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
98 | 97 | adantll 711 |
. . . . . . . . . 10
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
99 | 96, 98 | eqeq12d 2747 |
. . . . . . . . 9
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → (𝑏 = (𝐹‘𝑎) ↔ 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
100 | 99 | rexbidva 3175 |
. . . . . . . 8
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → (∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎) ↔ ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) |
101 | 95, 100 | mpbird 257 |
. . . . . . 7
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) |
102 | 101 | ex 412 |
. . . . . 6
⊢ ((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) |
103 | 102 | exlimivv 1934 |
. . . . 5
⊢
(∃𝑝∃𝑞(𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) |
104 | 14, 103 | syl 17 |
. . . 4
⊢ (𝑏 ∈ (𝐶 × 𝐼) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) |
105 | 104 | impcom 407 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐶 × 𝐼)) → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) |
106 | 105 | ralrimiva 3145 |
. 2
⊢ (𝜑 → ∀𝑏 ∈ (𝐶 × 𝐼)∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) |
107 | | dffo3 7103 |
. 2
⊢ (𝐹:𝐵–onto→(𝐶 × 𝐼) ↔ (𝐹:𝐵⟶(𝐶 × 𝐼) ∧ ∀𝑏 ∈ (𝐶 × 𝐼)∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) |
108 | 13, 106, 107 | sylanbrc 582 |
1
⊢ (𝜑 → 𝐹:𝐵–onto→(𝐶 × 𝐼)) |