Proof of Theorem ndmaovdistr
Step | Hyp | Ref
| Expression |
1 | | ndmaov.6 |
. . . . . . 7
⊢ dom 𝐺 = (𝑆 × 𝑆) |
2 | 1 | eleq2i 2680 |
. . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 ↔ 〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆)) |
3 | | opelxp 5070 |
. . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) |
4 | 2, 3 | bitri 263 |
. . . . 5
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) |
5 | | aovvdm 39914 |
. . . . . . 7
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → 〈𝐵, 𝐶〉 ∈ dom 𝐹) |
6 | | ndmaov.1 |
. . . . . . . . . 10
⊢ dom 𝐹 = (𝑆 × 𝑆) |
7 | 6 | eleq2i 2680 |
. . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ 〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆)) |
8 | | opelxp 5070 |
. . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆) ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
9 | 7, 8 | bitri 263 |
. . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
10 | | 3anass 1035 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
11 | 10 | simplbi2com 655 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
12 | 9, 11 | sylbi 206 |
. . . . . . 7
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
13 | 5, 12 | syl 17 |
. . . . . 6
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
14 | 13 | impcom 445 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
15 | 4, 14 | sylbi 206 |
. . . 4
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
16 | 15 | con3i 149 |
. . 3
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ¬ 〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺) |
17 | | ndmaov 39912 |
. . 3
⊢ (¬
〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐺 → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V) |
18 | 16, 17 | syl 17 |
. 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V) |
19 | 6 | eleq2i 2680 |
. . . . . 6
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 ↔ 〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ (𝑆 × 𝑆)) |
20 | | opelxp 5070 |
. . . . . 6
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ (𝑆 × 𝑆) ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆)) |
21 | 19, 20 | bitri 263 |
. . . . 5
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆)) |
22 | | aovvdm 39914 |
. . . . . . 7
⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → 〈𝐴, 𝐵〉 ∈ dom 𝐺) |
23 | 1 | eleq2i 2680 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 ↔ 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
24 | | opelxp 5070 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
25 | 23, 24 | bitri 263 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
26 | | aovvdm 39914 |
. . . . . . . . . 10
⊢ ( ((𝐴𝐺𝐶)) ∈ 𝑆 → 〈𝐴, 𝐶〉 ∈ dom 𝐺) |
27 | 1 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 ↔ 〈𝐴, 𝐶〉 ∈ (𝑆 × 𝑆)) |
28 | | opelxp 5070 |
. . . . . . . . . . . 12
⊢
(〈𝐴, 𝐶〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
29 | 27, 28 | bitri 263 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
30 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ∈ 𝑆) |
31 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐵 ∈ 𝑆) |
32 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐶 ∈ 𝑆) |
33 | 30, 31, 32 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
34 | 33 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
35 | 29, 34 | sylbi 206 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐶〉 ∈ dom 𝐺 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
36 | 26, 35 | syl 17 |
. . . . . . . . 9
⊢ ( ((𝐴𝐺𝐶)) ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
37 | 36 | com12 32 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
38 | 25, 37 | sylbi 206 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐺 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
39 | 22, 38 | syl 17 |
. . . . . 6
⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
40 | 39 | imp 444 |
. . . . 5
⊢ ((
((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
41 | 21, 40 | sylbi 206 |
. . . 4
⊢ (〈
((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
42 | 41 | con3i 149 |
. . 3
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ¬ 〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹) |
43 | | ndmaov 39912 |
. . 3
⊢ (¬
〈 ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) 〉 ∈ dom 𝐹 → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V) |
44 | 42, 43 | syl 17 |
. 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V) |
45 | 18, 44 | eqtr4d 2647 |
1
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) ) |