Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’ ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
2 | 1 | txbasex 22940 |
. . . . 5
β’ ((π β π β§ π β π) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β V) |
3 | | sssigagen 32808 |
. . . . 5
β’ (ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β V β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
4 | 2, 3 | syl 17 |
. . . 4
β’ ((π β π β§ π β π) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
5 | 4 | adantr 482 |
. . 3
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
6 | | eqid 2733 |
. . . . . 6
β’ (π΄ Γ π΅) = (π΄ Γ π΅) |
7 | | xpeq1 5651 |
. . . . . . . 8
β’ (π₯ = π΄ β (π₯ Γ π¦) = (π΄ Γ π¦)) |
8 | 7 | eqeq2d 2744 |
. . . . . . 7
β’ (π₯ = π΄ β ((π΄ Γ π΅) = (π₯ Γ π¦) β (π΄ Γ π΅) = (π΄ Γ π¦))) |
9 | | xpeq2 5658 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄ Γ π¦) = (π΄ Γ π΅)) |
10 | 9 | eqeq2d 2744 |
. . . . . . 7
β’ (π¦ = π΅ β ((π΄ Γ π΅) = (π΄ Γ π¦) β (π΄ Γ π΅) = (π΄ Γ π΅))) |
11 | 8, 10 | rspc2ev 3594 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π β§ (π΄ Γ π΅) = (π΄ Γ π΅)) β βπ₯ β π βπ¦ β π (π΄ Γ π΅) = (π₯ Γ π¦)) |
12 | 6, 11 | mp3an3 1451 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β βπ₯ β π βπ¦ β π (π΄ Γ π΅) = (π₯ Γ π¦)) |
13 | | xpexg 7688 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄ Γ π΅) β V) |
14 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) = (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
15 | 14 | elrnmpog 7495 |
. . . . . 6
β’ ((π΄ Γ π΅) β V β ((π΄ Γ π΅) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β βπ₯ β π βπ¦ β π (π΄ Γ π΅) = (π₯ Γ π¦))) |
16 | 13, 15 | syl 17 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β ((π΄ Γ π΅) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β βπ₯ β π βπ¦ β π (π΄ Γ π΅) = (π₯ Γ π¦))) |
17 | 12, 16 | mpbird 257 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β (π΄ Γ π΅) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
18 | 17 | adantl 483 |
. . 3
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄ Γ π΅) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
19 | 5, 18 | sseldd 3949 |
. 2
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄ Γ π΅) β (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
20 | 1 | sxval 32853 |
. . 3
β’ ((π β π β§ π β π) β (π Γs π) = (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
21 | 20 | adantr 482 |
. 2
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π Γs π) = (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
22 | 19, 21 | eleqtrrd 2837 |
1
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄ Γ π΅) β (π Γs π)) |