Step | Hyp | Ref
| Expression |
1 | | eqid 2795 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | | eqid 2795 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
3 | | oppglsm.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
4 | 1, 2, 3 | lsmfval 18493 |
. . . . . . 7
⊢ (𝐺 ∈ V → ⊕ =
(𝑢 ∈ 𝒫
(Base‘𝐺), 𝑡 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)))) |
5 | 4 | tposeqd 7746 |
. . . . . 6
⊢ (𝐺 ∈ V → tpos ⊕ = tpos
(𝑢 ∈ 𝒫
(Base‘𝐺), 𝑡 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)))) |
6 | | eqid 2795 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
7 | 6 | reldmmpo 7141 |
. . . . . . . . . . . 12
⊢ Rel dom
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
8 | 6 | mpofun 7132 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
9 | | funforn 6465 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) ↔ (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))) |
10 | 8, 9 | mpbi 231 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
11 | | tposfo2 7766 |
. . . . . . . . . . . 12
⊢ (Rel dom
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) → ((𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) → tpos (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):◡dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)))) |
12 | 7, 10, 11 | mp2 9 |
. . . . . . . . . . 11
⊢ tpos
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):◡dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
13 | | forn 6461 |
. . . . . . . . . . 11
⊢ (tpos
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)):◡dom (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))–onto→ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) → ran tpos (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran tpos
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = ran (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) |
15 | | oppglsm.o |
. . . . . . . . . . . . . . . 16
⊢ 𝑂 =
(oppg‘𝐺) |
16 | | eqid 2795 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑂) = (+g‘𝑂) |
17 | 2, 15, 16 | oppgplus 18218 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(+g‘𝑂)𝑦) = (𝑦(+g‘𝐺)𝑥) |
18 | 17 | eqcomi 2804 |
. . . . . . . . . . . . . 14
⊢ (𝑦(+g‘𝐺)𝑥) = (𝑥(+g‘𝑂)𝑦) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡) → (𝑦(+g‘𝐺)𝑥) = (𝑥(+g‘𝑂)𝑦)) |
20 | 19 | mpoeq3ia 7090 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = (𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑥(+g‘𝑂)𝑦)) |
21 | 20 | tposmpo 7780 |
. . . . . . . . . . 11
⊢ tpos
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) |
22 | 21 | rneqi 5689 |
. . . . . . . . . 10
⊢ ran tpos
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) |
23 | 14, 22 | eqtr3i 2821 |
. . . . . . . . 9
⊢ ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝒫
(Base‘𝐺) ∧ 𝑡 ∈ 𝒫
(Base‘𝐺)) → ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥)) = ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
25 | 24 | mpoeq3ia 7090 |
. . . . . . 7
⊢ (𝑢 ∈ 𝒫
(Base‘𝐺), 𝑡 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))) = (𝑢 ∈ 𝒫 (Base‘𝐺), 𝑡 ∈ 𝒫 (Base‘𝐺) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
26 | 25 | tposmpo 7780 |
. . . . . 6
⊢ tpos
(𝑢 ∈ 𝒫
(Base‘𝐺), 𝑡 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑦 ∈ 𝑢, 𝑥 ∈ 𝑡 ↦ (𝑦(+g‘𝐺)𝑥))) = (𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
27 | 5, 26 | syl6eq 2847 |
. . . . 5
⊢ (𝐺 ∈ V → tpos ⊕ =
(𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)))) |
28 | 15 | fvexi 6552 |
. . . . . 6
⊢ 𝑂 ∈ V |
29 | 15, 1 | oppgbas 18220 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝑂) |
30 | | eqid 2795 |
. . . . . . 7
⊢
(LSSum‘𝑂) =
(LSSum‘𝑂) |
31 | 29, 16, 30 | lsmfval 18493 |
. . . . . 6
⊢ (𝑂 ∈ V →
(LSSum‘𝑂) = (𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)))) |
32 | 28, 31 | ax-mp 5 |
. . . . 5
⊢
(LSSum‘𝑂) =
(𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
33 | 27, 32 | syl6reqr 2850 |
. . . 4
⊢ (𝐺 ∈ V →
(LSSum‘𝑂) = tpos
⊕
) |
34 | 33 | oveqd 7033 |
. . 3
⊢ (𝐺 ∈ V → (𝑇(LSSum‘𝑂)𝑈) = (𝑇tpos ⊕ 𝑈)) |
35 | | ovtpos 7758 |
. . 3
⊢ (𝑇tpos ⊕ 𝑈) = (𝑈 ⊕ 𝑇) |
36 | 34, 35 | syl6eq 2847 |
. 2
⊢ (𝐺 ∈ V → (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇)) |
37 | | eqid 2795 |
. . . . . . 7
⊢ (𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦
∅) = (𝑡 ∈
𝒫 (Base‘𝐺),
𝑢 ∈ 𝒫
(Base‘𝐺) ↦
∅) |
38 | | 0ex 5102 |
. . . . . . 7
⊢ ∅
∈ V |
39 | | eqidd 2796 |
. . . . . . 7
⊢ ((𝑡 = 𝑇 ∧ 𝑢 = 𝑈) → ∅ = ∅) |
40 | 37, 38, 39 | elovmpo 7249 |
. . . . . 6
⊢ (𝑥 ∈ (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) ↔ (𝑇 ∈ 𝒫 (Base‘𝐺) ∧ 𝑈 ∈ 𝒫 (Base‘𝐺) ∧ 𝑥 ∈ ∅)) |
41 | 40 | simp3bi 1140 |
. . . . 5
⊢ (𝑥 ∈ (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) → 𝑥 ∈ ∅) |
42 | 41 | ssriv 3893 |
. . . 4
⊢ (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) ⊆
∅ |
43 | | ss0 4272 |
. . . 4
⊢ ((𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) ⊆ ∅ → (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) = ∅) |
44 | 42, 43 | ax-mp 5 |
. . 3
⊢ (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈) = ∅ |
45 | | elpwi 4463 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫
(Base‘𝐺) → 𝑡 ⊆ (Base‘𝐺)) |
46 | 45 | 3ad2ant2 1127 |
. . . . . . . . . . . 12
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
𝑡 ⊆ (Base‘𝐺)) |
47 | | fvprc 6531 |
. . . . . . . . . . . . 13
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
48 | 47 | 3ad2ant1 1126 |
. . . . . . . . . . . 12
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
(Base‘𝐺) =
∅) |
49 | 46, 48 | sseqtrd 3928 |
. . . . . . . . . . 11
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
𝑡 ⊆
∅) |
50 | | ss0 4272 |
. . . . . . . . . . 11
⊢ (𝑡 ⊆ ∅ → 𝑡 = ∅) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
𝑡 =
∅) |
52 | | eqid 2795 |
. . . . . . . . . 10
⊢ 𝑢 = 𝑢 |
53 | | mpoeq12 7085 |
. . . . . . . . . 10
⊢ ((𝑡 = ∅ ∧ 𝑢 = 𝑢) → (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
54 | 51, 52, 53 | sylancl 586 |
. . . . . . . . 9
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) |
55 | | mpo0 7095 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = ∅ |
56 | 54, 55 | syl6eq 2847 |
. . . . . . . 8
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) →
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = ∅) |
57 | 56 | rneqd 5690 |
. . . . . . 7
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) → ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = ran ∅) |
58 | | rn0 5715 |
. . . . . . 7
⊢ ran
∅ = ∅ |
59 | 57, 58 | syl6eq 2847 |
. . . . . 6
⊢ ((¬
𝐺 ∈ V ∧ 𝑡 ∈ 𝒫
(Base‘𝐺) ∧ 𝑢 ∈ 𝒫
(Base‘𝐺)) → ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦)) = ∅) |
60 | 59 | mpoeq3dva 7089 |
. . . . 5
⊢ (¬
𝐺 ∈ V → (𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦ ran
(𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑂)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦
∅)) |
61 | 32, 60 | syl5eq 2843 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(LSSum‘𝑂) = (𝑡 ∈ 𝒫
(Base‘𝐺), 𝑢 ∈ 𝒫
(Base‘𝐺) ↦
∅)) |
62 | 61 | oveqd 7033 |
. . 3
⊢ (¬
𝐺 ∈ V → (𝑇(LSSum‘𝑂)𝑈) = (𝑇(𝑡 ∈ 𝒫 (Base‘𝐺), 𝑢 ∈ 𝒫 (Base‘𝐺) ↦ ∅)𝑈)) |
63 | | fvprc 6531 |
. . . . . 6
⊢ (¬
𝐺 ∈ V →
(LSSum‘𝐺) =
∅) |
64 | 3, 63 | syl5eq 2843 |
. . . . 5
⊢ (¬
𝐺 ∈ V → ⊕ =
∅) |
65 | 64 | oveqd 7033 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑈 ⊕ 𝑇) = (𝑈∅𝑇)) |
66 | | 0ov 7052 |
. . . 4
⊢ (𝑈∅𝑇) = ∅ |
67 | 65, 66 | syl6eq 2847 |
. . 3
⊢ (¬
𝐺 ∈ V → (𝑈 ⊕ 𝑇) = ∅) |
68 | 44, 62, 67 | 3eqtr4a 2857 |
. 2
⊢ (¬
𝐺 ∈ V → (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇)) |
69 | 36, 68 | pm2.61i 183 |
1
⊢ (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇) |