Proof of Theorem ndmaovdistr
Step | Hyp | Ref
| Expression |
1 | | ndmaov.6 |
. . . . . . 7
⊢ dom 𝐺 = (𝑆 × 𝑆) |
2 | 1 | eleq2i 2851 |
. . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 ↔ 〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆)) |
3 | | opelxp 5391 |
. . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) |
4 | 2, 3 | bitri 267 |
. . . . 5
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) |
5 | | aovvdm 42230 |
. . . . . . 7
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → 〈𝐵, 𝐶〉 ∈ dom 𝐹) |
6 | | ndmaov.1 |
. . . . . . . . . 10
⊢ dom 𝐹 = (𝑆 × 𝑆) |
7 | 6 | eleq2i 2851 |
. . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ 〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆)) |
8 | | opelxp 5391 |
. . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆) ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
9 | 7, 8 | bitri 267 |
. . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
10 | | 3anass 1079 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
11 | 10 | simplbi2com 498 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
12 | 9, 11 | sylbi 209 |
. . . . . . 7
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
13 | 5, 12 | syl 17 |
. . . . . 6
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
14 | 13 | impcom 398 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
15 | 4, 14 | sylbi 209 |
. . . 4
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
16 | 15 | con3i 152 |
. . 3
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ¬ 〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺) |
17 | | ndmaov 42228 |
. . 3
⊢ (¬
〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V) |
18 | 16, 17 | syl 17 |
. 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V) |
19 | 6 | eleq2i 2851 |
. . . . . 6
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 ↔ 〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ (𝑆 × 𝑆)) |
20 | | opelxp 5391 |
. . . . . 6
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ (𝑆 × 𝑆) ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆)) |
21 | 19, 20 | bitri 267 |
. . . . 5
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆)) |
22 | | aovvdm 42230 |
. . . . . . 7
⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → 〈𝐴, 𝐵〉 ∈ dom 𝐺) |
23 | 1 | eleq2i 2851 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 ↔ 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
24 | | opelxp 5391 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
25 | 23, 24 | bitri 267 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
26 | 1 | eleq2i 2851 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 ↔ 〈𝐴, 𝐶〉 ∈ (𝑆 × 𝑆)) |
27 | | opelxp 5391 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐶〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
28 | 26, 27 | bitri 267 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
29 | | simpll 757 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ∈ 𝑆) |
30 | | simprr 763 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐵 ∈ 𝑆) |
31 | | simplr 759 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐶 ∈ 𝑆) |
32 | 29, 30, 31 | 3jca 1119 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
33 | 32 | ex 403 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
34 | 28, 33 | sylbi 209 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
35 | | aovvdm 42230 |
. . . . . . . . 9
⊢ ( ((𝐴𝐺𝐶)) ∈ 𝑆 → 〈𝐴, 𝐶〉 ∈ dom 𝐺) |
36 | 34, 35 | syl11 33 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
37 | 25, 36 | sylbi 209 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
38 | 22, 37 | syl 17 |
. . . . . 6
⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
39 | 38 | imp 397 |
. . . . 5
⊢ ((
((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
40 | 21, 39 | sylbi 209 |
. . . 4
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
41 | 40 | con3i 152 |
. . 3
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ¬ 〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹) |
42 | | ndmaov 42228 |
. . 3
⊢ (¬
〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V) |
43 | 41, 42 | syl 17 |
. 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V) |
44 | 18, 43 | eqtr4d 2817 |
1
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) ) |