Step | Hyp | Ref
| Expression |
1 | | distrnq 10904 |
. . . 4
โข (๐ด
ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) = ((๐ด
ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) |
2 | | distrnq 10904 |
. . . . . . . 8
โข
((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) =
(((1Q +Q
1Q) ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q ((1Q
+Q 1Q)
ยทQ
(*Qโ(1Q
+Q 1Q)))) |
3 | | 1nq 10871 |
. . . . . . . . . . 11
โข
1Q โ Q |
4 | | addclnq 10888 |
. . . . . . . . . . 11
โข
((1Q โ Q โง
1Q โ Q) โ
(1Q +Q
1Q) โ Q) |
5 | 3, 3, 4 | mp2an 691 |
. . . . . . . . . 10
โข
(1Q +Q
1Q) โ Q |
6 | | recidnq 10908 |
. . . . . . . . . 10
โข
((1Q +Q
1Q) โ Q โ
((1Q +Q
1Q) ยทQ
(*Qโ(1Q
+Q 1Q))) =
1Q) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
โข
((1Q +Q
1Q) ยทQ
(*Qโ(1Q
+Q 1Q))) =
1Q |
8 | 7, 7 | oveq12i 7374 |
. . . . . . . 8
โข
(((1Q +Q
1Q) ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q ((1Q
+Q 1Q)
ยทQ
(*Qโ(1Q
+Q 1Q)))) =
(1Q +Q
1Q) |
9 | 2, 8 | eqtri 2765 |
. . . . . . 7
โข
((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) =
(1Q +Q
1Q) |
10 | 9 | oveq1i 7372 |
. . . . . 6
โข
(((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))))
ยทQ
(*Qโ(1Q
+Q 1Q))) =
((1Q +Q
1Q) ยทQ
(*Qโ(1Q
+Q 1Q))) |
11 | 7 | oveq2i 7373 |
. . . . . . 7
โข
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ ((1Q
+Q 1Q)
ยทQ
(*Qโ(1Q
+Q 1Q)))) =
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ
1Q) |
12 | | mulassnq 10902 |
. . . . . . . 8
โข
((((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ (1Q
+Q 1Q))
ยทQ
(*Qโ(1Q
+Q 1Q))) =
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ ((1Q
+Q 1Q)
ยทQ
(*Qโ(1Q
+Q 1Q)))) |
13 | | mulcomnq 10896 |
. . . . . . . . 9
โข
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ (1Q
+Q 1Q)) =
((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) |
14 | 13 | oveq1i 7372 |
. . . . . . . 8
โข
((((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ (1Q
+Q 1Q))
ยทQ
(*Qโ(1Q
+Q 1Q))) =
(((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))))
ยทQ
(*Qโ(1Q
+Q 1Q))) |
15 | 12, 14 | eqtr3i 2767 |
. . . . . . 7
โข
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ ((1Q
+Q 1Q)
ยทQ
(*Qโ(1Q
+Q 1Q)))) =
(((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))))
ยทQ
(*Qโ(1Q
+Q 1Q))) |
16 | | recclnq 10909 |
. . . . . . . . 9
โข
((1Q +Q
1Q) โ Q โ
(*Qโ(1Q
+Q 1Q)) โ
Q) |
17 | | addclnq 10888 |
. . . . . . . . 9
โข
(((*Qโ(1Q
+Q 1Q)) โ
Q โง
(*Qโ(1Q
+Q 1Q)) โ
Q) โ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) โ
Q) |
18 | 16, 16, 17 | syl2anc 585 |
. . . . . . . 8
โข
((1Q +Q
1Q) โ Q โ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) โ
Q) |
19 | | mulidnq 10906 |
. . . . . . . 8
โข
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) โ
Q โ
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ 1Q) =
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) |
20 | 5, 18, 19 | mp2b 10 |
. . . . . . 7
โข
(((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))
ยทQ 1Q) =
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) |
21 | 11, 15, 20 | 3eqtr3i 2773 |
. . . . . 6
โข
(((1Q +Q
1Q) ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))))
ยทQ
(*Qโ(1Q
+Q 1Q))) =
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) |
22 | 10, 21, 7 | 3eqtr3i 2773 |
. . . . 5
โข
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q))) =
1Q |
23 | 22 | oveq2i 7373 |
. . . 4
โข (๐ด
ยทQ
((*Qโ(1Q
+Q 1Q))
+Q
(*Qโ(1Q
+Q 1Q)))) = (๐ด
ยทQ
1Q) |
24 | 1, 23 | eqtr3i 2767 |
. . 3
โข ((๐ด
ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) = (๐ด
ยทQ
1Q) |
25 | | mulidnq 10906 |
. . 3
โข (๐ด โ Q โ
(๐ด
ยทQ 1Q) = ๐ด) |
26 | 24, 25 | eqtrid 2789 |
. 2
โข (๐ด โ Q โ
((๐ด
ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) = ๐ด) |
27 | | ovex 7395 |
. . 3
โข (๐ด
ยทQ
(*Qโ(1Q
+Q 1Q))) โ
V |
28 | | oveq12 7371 |
. . . . 5
โข ((๐ฅ = (๐ด ยทQ
(*Qโ(1Q
+Q 1Q))) โง ๐ฅ = (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) โ (๐ฅ +Q
๐ฅ) = ((๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q))))) |
29 | 28 | anidms 568 |
. . . 4
โข (๐ฅ = (๐ด ยทQ
(*Qโ(1Q
+Q 1Q))) โ (๐ฅ +Q
๐ฅ) = ((๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q))))) |
30 | 29 | eqeq1d 2739 |
. . 3
โข (๐ฅ = (๐ด ยทQ
(*Qโ(1Q
+Q 1Q))) โ ((๐ฅ +Q
๐ฅ) = ๐ด โ ((๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) = ๐ด)) |
31 | 27, 30 | spcev 3568 |
. 2
โข (((๐ด
ยทQ
(*Qโ(1Q
+Q 1Q)))
+Q (๐ด ยทQ
(*Qโ(1Q
+Q 1Q)))) = ๐ด โ โ๐ฅ(๐ฅ +Q ๐ฅ) = ๐ด) |
32 | 26, 31 | syl 17 |
1
โข (๐ด โ Q โ
โ๐ฅ(๐ฅ +Q ๐ฅ) = ๐ด) |